update

binghe · Oct 25, 2024 · 23f099c · 23f099c
1 parent 34186ab
commit 23f099c
Show file tree

Hide file tree

Showing 2 changed files with 746 additions and 4 deletions.
diff --git a/examples/Crypto/RC5/rc5Script.sml b/examples/Crypto/RC5/rc5Script.sml
@@ -1,15 +1,15 @@
 (*===========================================================================*)
-(*  The Data Encryption Standard (DES) in HOL                                *)
+(*  The RC5 in HOL                                *)
 (*===========================================================================*)
 
 open HolKernel Parse boolLib bossLib;
 
 open arithmeticTheory numLib pairTheory fcpTheory fcpLib wordsTheory wordsLib
      listTheory listLib sortingTheory pred_setTheory combinTheory hurdUtils;
 
-val _ = guessing_word_lengths := true;
-val _ = new_theory "rc5";
 
+val _ = new_theory "rc5";
+val _ = guessing_word_lengths := true;
 val fcp_ss = std_ss ++ fcpLib.FCP_ss;
 Type    block[pp] = “:word32 # word32”
 (* Data Table *)
@@ -577,5 +577,5 @@ Proof
 QED
 
 val _ = export_theory();
-val _ = html_theory "RC5";
+val _ = html_theory "rc5";