Updated snapshots for Isabelle 2018

30 files changed, 365 insertions, 370 deletions

diff --git a/snapshots/isabelle/lib/lem/Lem.thy b/snapshots/isabelle/lib/lem/Lem.thy
index c6a2a883..ae2c2f2d 100644
--- a/snapshots/isabelle/lib/lem/Lem.thy
+++ b/snapshots/isabelle/lib/lem/Lem.thy
@@ -57,7 +57,7 @@ theory "Lem"
 
 imports
          LemExtraDefs
-         "~~/src/HOL/Word/Word"
+         "HOL-Word.Word"
 begin
 
 type_synonym numeral = nat
diff --git a/snapshots/isabelle/lib/lem/LemExtraDefs.thy b/snapshots/isabelle/lib/lem/LemExtraDefs.thy
index c14a669f..e43ff663 100644
--- a/snapshots/isabelle/lib/lem/LemExtraDefs.thy
+++ b/snapshots/isabelle/lib/lem/LemExtraDefs.thy
@@ -56,9 +56,9 @@ chapter \<open>Auxiliary Definitions needed by Lem\<close>
 theory "LemExtraDefs"
 
 imports
- 	 Main
-   "~~/src/HOL/Library/Permutation"
-   "~~/src/HOL/Library/While_Combinator"
+   Main
+   "HOL-Library.Permutation"
+   "HOL-Library.While_Combinator"
 begin
 
 subsection \<open>General\<close>
@@ -109,7 +109,7 @@ by (induct l) auto
 
 lemma sorted_map_suc :
   "sorted l \<Longrightarrow> sorted (map Suc l)"
-by (induct l) (simp_all add: sorted_Cons)
+by (induct l) (simp_all)
 
 lemma sorted_find_indices :
   "sorted (find_indices P xs)"
@@ -119,7 +119,7 @@ next
   case (Cons x xs)
   from sorted_map_suc[OF this]
   show ?case
-    by (simp add: sorted_Cons)
+    by (simp)
 qed
 
 lemma find_indices_set [simp] :
@@ -159,7 +159,7 @@ next
 
   from sorted_find_indices[of P xs] find_indices_eq
   have "sorted (i # il)" by simp
-  hence i_leq: "\<And>i'. i' \<in> set (i # il) \<Longrightarrow> i \<le> i'" unfolding sorted_Cons by auto
+  hence i_leq: "\<And>i'. i' \<in> set (i # il) \<Longrightarrow> i \<le> i'" by auto
 
   from find_indices_set[of P xs, unfolded find_indices_eq]
   have set_i_il_eq:"\<And>i'. i' \<in> set (i # il) = (i' < length xs \<and> P (xs ! i'))"
@@ -342,15 +342,15 @@ fun sorted_by  :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list
  | "sorted_by cmp (x1 # x2 # xs) = ((cmp x1 x2) \<and> sorted_by cmp (x2 # xs))"
 
 lemma sorted_by_lesseq [simp] :
-  "sorted_by ((op \<le>) :: ('a::{linorder}) => 'a => bool) = sorted"
+  "sorted_by ((\<le>) :: ('a::{linorder}) => 'a => bool) = sorted"
 proof (rule ext)
   fix l :: "'a list"
-  show "sorted_by (op \<le>) l = sorted l"
+  show "sorted_by (\<le>) l = sorted l"
   proof (induct l)
     case Nil thus ?case by simp
   next
     case (Cons x xs)
-    thus ?case by (cases xs) (simp_all)
+    thus ?case by (cases xs) (simp_all del: sorted.simps(2) add: sorted2_simps)
   qed
 qed
 
@@ -688,7 +688,7 @@ next
       thus ?thesis by blast
     next
       case False
-      with xyl_in have "xyl \<in> op # y ` insert_in_list_at_arbitrary_pos x l" by simp
+      with xyl_in have "xyl \<in> (#) y ` insert_in_list_at_arbitrary_pos x l" by simp
       with ind_hyp obtain l1 l2 where "l = l1 @ l2 \<and> xyl = y # l1 @ x # l2"
          by (auto simp add: image_def Bex_def)
       hence "y # l = (y # l1) @ l2 \<and> xyl = (y # l1) @ [x] @ l2" by simp
@@ -857,16 +857,12 @@ subsection \<open>sorting\<close>
 
 subsection \<open>Strings\<close>
 
-lemma explode_str_simp [simp] :
-  "String.explode (STR l) = l"
-by (metis STR_inverse UNIV_I)
-
 declare String.literal.explode_inverse [simp]
 
 subsection \<open>num to string conversions\<close>
 
 definition nat_list_to_string :: "nat list \<Rightarrow> string" where
-  "nat_list_to_string nl = map char_of_nat nl"
+  "nat_list_to_string nl = map char_of nl"
 
 definition is_digit where
   "is_digit (n::nat) = (n < 10)"
diff --git a/snapshots/isabelle/lib/lem/Lem_assert_extra.thy b/snapshots/isabelle/lib/lem/Lem_assert_extra.thy
index b56e5a19..9dedb07a 100644
--- a/snapshots/isabelle/lib/lem/Lem_assert_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_assert_extra.thy
@@ -1,10 +1,10 @@
-chapter \<open>Generated by Lem from assert_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>assert_extra.lem\<close>.\<close>
 
 theory "Lem_assert_extra" 
 
-imports 
- 	 Main
-	 "Lem" 
+imports
+  Main
+  "Lem"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_basic_classes.thy b/snapshots/isabelle/lib/lem/Lem_basic_classes.thy
index c23da22b..5719357c 100644
--- a/snapshots/isabelle/lib/lem/Lem_basic_classes.thy
+++ b/snapshots/isabelle/lib/lem/Lem_basic_classes.thy
@@ -1,10 +1,10 @@
-chapter \<open>Generated by Lem from basic_classes.lem.\<close>
+chapter \<open>Generated by Lem from \<open>basic_classes.lem\<close>.\<close>
 
 theory "Lem_basic_classes" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
+imports
+  Main
+  "Lem_bool"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_bool.thy b/snapshots/isabelle/lib/lem/Lem_bool.thy
index 75142160..960286a3 100644
--- a/snapshots/isabelle/lib/lem/Lem_bool.thy
+++ b/snapshots/isabelle/lib/lem/Lem_bool.thy
@@ -1,9 +1,9 @@
-chapter \<open>Generated by Lem from bool.lem.\<close>
+chapter \<open>Generated by Lem from \<open>bool.lem\<close>.\<close>
 
 theory "Lem_bool" 
 
-imports 
- 	 Main
+imports
+  Main
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_either.thy b/snapshots/isabelle/lib/lem/Lem_either.thy
index e181f823..24fe6d67 100644
--- a/snapshots/isabelle/lib/lem/Lem_either.thy
+++ b/snapshots/isabelle/lib/lem/Lem_either.thy
@@ -1,13 +1,13 @@
-chapter \<open>Generated by Lem from either.lem.\<close>
+chapter \<open>Generated by Lem from \<open>either.lem\<close>.\<close>
 
 theory "Lem_either" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_list" 
-	 "Lem_tuple" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_list"
+  "Lem_tuple"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_function.thy b/snapshots/isabelle/lib/lem/Lem_function.thy
index 29c1fb04..b8ce9ae7 100644
--- a/snapshots/isabelle/lib/lem/Lem_function.thy
+++ b/snapshots/isabelle/lib/lem/Lem_function.thy
@@ -1,11 +1,11 @@
-chapter \<open>Generated by Lem from function.lem.\<close>
+chapter \<open>Generated by Lem from \<open>function.lem\<close>.\<close>
 
 theory "Lem_function" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_function_extra.thy b/snapshots/isabelle/lib/lem/Lem_function_extra.thy
index f742e1e6..7ed34eeb 100644
--- a/snapshots/isabelle/lib/lem/Lem_function_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_function_extra.thy
@@ -1,15 +1,15 @@
-chapter \<open>Generated by Lem from function_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>function_extra.lem\<close>.\<close>
 
 theory "Lem_function_extra" 
 
-imports 
- 	 Main
-	 "Lem_maybe" 
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_num" 
-	 "Lem_function" 
-	 "Lem" 
+imports
+  Main
+  "Lem_maybe"
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_num"
+  "Lem_function"
+  "Lem"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_list.thy b/snapshots/isabelle/lib/lem/Lem_list.thy
index 3bdef057..1e49be6e 100644
--- a/snapshots/isabelle/lib/lem/Lem_list.thy
+++ b/snapshots/isabelle/lib/lem/Lem_list.thy
@@ -1,16 +1,16 @@
-chapter \<open>Generated by Lem from list.lem.\<close>
+chapter \<open>Generated by Lem from \<open>list.lem\<close>.\<close>
 
 theory "Lem_list" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_maybe" 
-	 "Lem_basic_classes" 
-	 "Lem_function" 
-	 "Lem_tuple" 
-	 "Lem_num" 
-	 "Lem" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_maybe"
+  "Lem_basic_classes"
+  "Lem_function"
+  "Lem_tuple"
+  "Lem_num"
+  "Lem"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_list_extra.thy b/snapshots/isabelle/lib/lem/Lem_list_extra.thy
index 9caf32fc..43806c73 100644
--- a/snapshots/isabelle/lib/lem/Lem_list_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_list_extra.thy
@@ -1,16 +1,16 @@
-chapter \<open>Generated by Lem from list_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>list_extra.lem\<close>.\<close>
 
 theory "Lem_list_extra" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_maybe" 
-	 "Lem_basic_classes" 
-	 "Lem_tuple" 
-	 "Lem_num" 
-	 "Lem_list" 
-	 "Lem_assert_extra" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_maybe"
+  "Lem_basic_classes"
+  "Lem_tuple"
+  "Lem_num"
+  "Lem_list"
+  "Lem_assert_extra"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_machine_word.thy b/snapshots/isabelle/lib/lem/Lem_machine_word.thy
index 85323bb2..d05e3876 100644
--- a/snapshots/isabelle/lib/lem/Lem_machine_word.thy
+++ b/snapshots/isabelle/lib/lem/Lem_machine_word.thy
@@ -1,15 +1,15 @@
-chapter \<open>Generated by Lem from machine_word.lem.\<close>
+chapter \<open>Generated by Lem from \<open>machine_word.lem\<close>.\<close>
 
 theory "Lem_machine_word" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_num" 
-	 "Lem_basic_classes" 
-	 "Lem_show" 
-	 "Lem_function" 
-	 "~~/src/HOL/Word/Word" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_num"
+  "Lem_basic_classes"
+  "Lem_show"
+  "Lem_function"
+  "HOL-Word.Word"
 
 begin 
 
@@ -17,7 +17,7 @@ begin
 
 (*open import Bool Num Basic_classes Show Function*)
 
-(*open import {isabelle} `~~/src/HOL/Word/Word`*)
+(*open import {isabelle} `HOL-Word.Word`*)
 (*open import {hol} `wordsTheory` `wordsLib` `bitstringTheory` `integer_wordTheory`*)
 
 (*type mword 'a*)
diff --git a/snapshots/isabelle/lib/lem/Lem_map.thy b/snapshots/isabelle/lib/lem/Lem_map.thy
index fbaed71a..ada694f3 100644
--- a/snapshots/isabelle/lib/lem/Lem_map.thy
+++ b/snapshots/isabelle/lib/lem/Lem_map.thy
@@ -1,17 +1,17 @@
-chapter \<open>Generated by Lem from map.lem.\<close>
+chapter \<open>Generated by Lem from \<open>map.lem\<close>.\<close>
 
 theory "Lem_map" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_function" 
-	 "Lem_maybe" 
-	 "Lem_list" 
-	 "Lem_tuple" 
-	 "Lem_set" 
-	 "Lem_num" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_function"
+  "Lem_maybe"
+  "Lem_list"
+  "Lem_tuple"
+  "Lem_set"
+  "Lem_num"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_map_extra.thy b/snapshots/isabelle/lib/lem/Lem_map_extra.thy
index 4117fe81..1ed4b531 100644
--- a/snapshots/isabelle/lib/lem/Lem_map_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_map_extra.thy
@@ -1,18 +1,18 @@
-chapter \<open>Generated by Lem from map_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>map_extra.lem\<close>.\<close>
 
 theory "Lem_map_extra" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_function" 
-	 "Lem_assert_extra" 
-	 "Lem_maybe" 
-	 "Lem_list" 
-	 "Lem_num" 
-	 "Lem_set" 
-	 "Lem_map" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_function"
+  "Lem_assert_extra"
+  "Lem_maybe"
+  "Lem_list"
+  "Lem_num"
+  "Lem_set"
+  "Lem_map"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_maybe.thy b/snapshots/isabelle/lib/lem/Lem_maybe.thy
index da0bde92..6ee955c2 100644
--- a/snapshots/isabelle/lib/lem/Lem_maybe.thy
+++ b/snapshots/isabelle/lib/lem/Lem_maybe.thy
@@ -1,12 +1,12 @@
-chapter \<open>Generated by Lem from maybe.lem.\<close>
+chapter \<open>Generated by Lem from \<open>maybe.lem\<close>.\<close>
 
 theory "Lem_maybe" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_function" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_function"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy b/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy
index 0a57814c..80ea494f 100644
--- a/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy
@@ -1,12 +1,12 @@
-chapter \<open>Generated by Lem from maybe_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>maybe_extra.lem\<close>.\<close>
 
 theory "Lem_maybe_extra" 
 
-imports 
- 	 Main
-	 "Lem_basic_classes" 
-	 "Lem_maybe" 
-	 "Lem_assert_extra" 
+imports
+  Main
+  "Lem_basic_classes"
+  "Lem_maybe"
+  "Lem_assert_extra"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_num.thy b/snapshots/isabelle/lib/lem/Lem_num.thy
index ddbdd533..8efe867b 100644
--- a/snapshots/isabelle/lib/lem/Lem_num.thy
+++ b/snapshots/isabelle/lib/lem/Lem_num.thy
@@ -1,21 +1,20 @@
-chapter \<open>Generated by Lem from num.lem.\<close>
+chapter \<open>Generated by Lem from \<open>num.lem\<close>.\<close>
 
 theory "Lem_num" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "~~/src/HOL/Word/Word" 
-	 "Real" 
-	 "~~/src/HOL/NthRoot" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "HOL-Word.Word"
+  "Complex_Main"
 
 begin 
 
 
 
 (*open import Bool Basic_classes*)
-(*open import {isabelle} `~~/src/HOL/Word/Word` `Real` `~~/src/HOL/NthRoot`*)
+(*open import {isabelle} `HOL-Word.Word` `Complex_Main`*)
 (*open import {hol} `integerTheory` `intReduce` `wordsTheory` `wordsLib` `ratTheory` `realTheory` `intrealTheory` `transcTheory`*)
 (*open import {coq} `Coq.Numbers.BinNums` `Coq.ZArith.BinInt` `Coq.ZArith.Zpower` `Coq.ZArith.Zdiv` `Coq.ZArith.Zmax` `Coq.Numbers.Natural.Peano.NPeano` `Coq.QArith.Qabs` `Coq.QArith.Qminmax` `Coq.QArith.Qround` `Coq.Reals.ROrderedType` `Coq.Reals.Rbase` `Coq.Reals.Rfunctions`*) 
 
@@ -188,15 +187,15 @@ record 'a NumPred_class=
 definition instance_Basic_classes_Ord_nat_dict  :: "(nat)Ord_class "  where 
      " instance_Basic_classes_Ord_nat_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val natAdd : nat -> nat -> nat*)
@@ -204,7 +203,7 @@ definition instance_Basic_classes_Ord_nat_dict  :: "(nat)Ord_class "  where
 definition instance_Num_NumAdd_nat_dict  :: "(nat)NumAdd_class "  where 
      " instance_Num_NumAdd_nat_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val natMinus : nat -> nat -> nat*)
@@ -212,7 +211,7 @@ definition instance_Num_NumAdd_nat_dict  :: "(nat)NumAdd_class "  where
 definition instance_Num_NumMinus_nat_dict  :: "(nat)NumMinus_class "  where 
      " instance_Num_NumMinus_nat_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val natSucc : nat -> nat*)
@@ -235,7 +234,7 @@ definition instance_Num_NumPred_nat_dict  :: "(nat)NumPred_class "  where
 definition instance_Num_NumMult_nat_dict  :: "(nat)NumMult_class "  where 
      " instance_Num_NumMult_nat_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 (*val natDiv : nat -> nat -> nat*)
@@ -243,13 +242,13 @@ definition instance_Num_NumMult_nat_dict  :: "(nat)NumMult_class "  where
 definition instance_Num_NumIntegerDivision_nat_dict  :: "(nat)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_nat_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_nat_dict  :: "(nat)NumDivision_class "  where 
      " instance_Num_NumDivision_nat_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val natMod : nat -> nat -> nat*)
@@ -257,7 +256,7 @@ definition instance_Num_NumDivision_nat_dict  :: "(nat)NumDivision_class "  wher
 definition instance_Num_NumRemainder_nat_dict  :: "(nat)NumRemainder_class "  where 
      " instance_Num_NumRemainder_nat_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 
@@ -284,7 +283,7 @@ definition gen_pow  :: " 'a \<Rightarrow>('a \<Rightarrow> 'a \<Rightarrow> 'a)\
 definition instance_Num_NumPow_nat_dict  :: "(nat)NumPow_class "  where 
      " instance_Num_NumPow_nat_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val natMin : nat -> nat -> nat*)
@@ -318,15 +317,15 @@ definition instance_Basic_classes_OrdMaxMin_nat_dict  :: "(nat)OrdMaxMin_class "
 definition instance_Basic_classes_Ord_Num_natural_dict  :: "(nat)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_natural_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val naturalAdd : natural -> natural -> natural*)
@@ -334,7 +333,7 @@ definition instance_Basic_classes_Ord_Num_natural_dict  :: "(nat)Ord_class "  wh
 definition instance_Num_NumAdd_Num_natural_dict  :: "(nat)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_natural_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val naturalMinus : natural -> natural -> natural*)
@@ -342,7 +341,7 @@ definition instance_Num_NumAdd_Num_natural_dict  :: "(nat)NumAdd_class "  where
 definition instance_Num_NumMinus_Num_natural_dict  :: "(nat)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_natural_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val naturalSucc : natural -> natural*)
@@ -365,7 +364,7 @@ definition instance_Num_NumPred_Num_natural_dict  :: "(nat)NumPred_class "  wher
 definition instance_Num_NumMult_Num_natural_dict  :: "(nat)NumMult_class "  where 
      " instance_Num_NumMult_Num_natural_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 
@@ -374,7 +373,7 @@ definition instance_Num_NumMult_Num_natural_dict  :: "(nat)NumMult_class "  wher
 definition instance_Num_NumPow_Num_natural_dict  :: "(nat)NumPow_class "  where 
      " instance_Num_NumPow_Num_natural_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val naturalDiv : natural -> natural -> natural*)
@@ -382,13 +381,13 @@ definition instance_Num_NumPow_Num_natural_dict  :: "(nat)NumPow_class "  where
 definition instance_Num_NumIntegerDivision_Num_natural_dict  :: "(nat)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_Num_natural_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_Num_natural_dict  :: "(nat)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_natural_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val naturalMod : natural -> natural -> natural*)
@@ -396,7 +395,7 @@ definition instance_Num_NumDivision_Num_natural_dict  :: "(nat)NumDivision_class
 definition instance_Num_NumRemainder_Num_natural_dict  :: "(nat)NumRemainder_class "  where 
      " instance_Num_NumRemainder_Num_natural_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 (*val naturalMin : natural -> natural -> natural*)
@@ -430,15 +429,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_natural_dict  :: "(nat)OrdMaxMin
 definition instance_Basic_classes_Ord_Num_int_dict  :: "(int)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_int_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val intNegate : int -> int*)
@@ -462,7 +461,7 @@ definition instance_Num_NumAbs_Num_int_dict  :: "(int)NumAbs_class "  where
 definition instance_Num_NumAdd_Num_int_dict  :: "(int)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_int_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val intMinus : int -> int -> int*)
@@ -470,7 +469,7 @@ definition instance_Num_NumAdd_Num_int_dict  :: "(int)NumAdd_class "  where
 definition instance_Num_NumMinus_Num_int_dict  :: "(int)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_int_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val intSucc : int -> int*)
@@ -492,7 +491,7 @@ definition instance_Num_NumPred_Num_int_dict  :: "(int)NumPred_class "  where
 definition instance_Num_NumMult_Num_int_dict  :: "(int)NumMult_class "  where 
      " instance_Num_NumMult_Num_int_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 
@@ -501,7 +500,7 @@ definition instance_Num_NumMult_Num_int_dict  :: "(int)NumMult_class "  where
 definition instance_Num_NumPow_Num_int_dict  :: "(int)NumPow_class "  where 
      " instance_Num_NumPow_Num_int_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val intDiv : int -> int -> int*)
@@ -509,13 +508,13 @@ definition instance_Num_NumPow_Num_int_dict  :: "(int)NumPow_class "  where
 definition instance_Num_NumIntegerDivision_Num_int_dict  :: "(int)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_Num_int_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_Num_int_dict  :: "(int)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_int_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val intMod : int -> int -> int*)
@@ -523,7 +522,7 @@ definition instance_Num_NumDivision_Num_int_dict  :: "(int)NumDivision_class "
 definition instance_Num_NumRemainder_Num_int_dict  :: "(int)NumRemainder_class "  where 
      " instance_Num_NumRemainder_Num_int_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 (*val intMin : int -> int -> int*)
@@ -555,7 +554,7 @@ definition instance_Basic_classes_OrdMaxMin_Num_int_dict  :: "(int)OrdMaxMin_cla
 definition instance_Basic_classes_Ord_Num_int32_dict  :: "( 32 word)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_int32_dict = ((|
 
-  compare_method = (genericCompare word_sless (op=)),
+  compare_method = (genericCompare word_sless (=)),
 
   isLess_method = word_sless,
 
@@ -591,7 +590,7 @@ definition instance_Num_NumAbs_Num_int32_dict  :: "( 32 word)NumAbs_class "  whe
 definition instance_Num_NumAdd_Num_int32_dict  :: "( 32 word)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_int32_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val int32Minus : int32 -> int32 -> int32*)
@@ -599,7 +598,7 @@ definition instance_Num_NumAdd_Num_int32_dict  :: "( 32 word)NumAdd_class "  whe
 definition instance_Num_NumMinus_Num_int32_dict  :: "( 32 word)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_int32_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val int32Succ : int32 -> int32*)
@@ -622,7 +621,7 @@ definition instance_Num_NumPred_Num_int32_dict  :: "( 32 word)NumPred_class "  w
 definition instance_Num_NumMult_Num_int32_dict  :: "( 32 word)NumMult_class "  where 
      " instance_Num_NumMult_Num_int32_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 
@@ -631,7 +630,7 @@ definition instance_Num_NumMult_Num_int32_dict  :: "( 32 word)NumMult_class "  w
 definition instance_Num_NumPow_Num_int32_dict  :: "( 32 word)NumPow_class "  where 
      " instance_Num_NumPow_Num_int32_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val int32Div : int32 -> int32 -> int32*)
@@ -639,13 +638,13 @@ definition instance_Num_NumPow_Num_int32_dict  :: "( 32 word)NumPow_class "  whe
 definition instance_Num_NumIntegerDivision_Num_int32_dict  :: "( 32 word)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_Num_int32_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_Num_int32_dict  :: "( 32 word)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_int32_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val int32Mod : int32 -> int32 -> int32*)
@@ -653,7 +652,7 @@ definition instance_Num_NumDivision_Num_int32_dict  :: "( 32 word)NumDivision_cl
 definition instance_Num_NumRemainder_Num_int32_dict  :: "( 32 word)NumRemainder_class "  where 
      " instance_Num_NumRemainder_Num_int32_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 (*val int32Min : int32 -> int32 -> int32*)
@@ -687,7 +686,7 @@ definition instance_Basic_classes_OrdMaxMin_Num_int32_dict  :: "( 32 word)OrdMax
 definition instance_Basic_classes_Ord_Num_int64_dict  :: "( 64 word)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_int64_dict = ((|
 
-  compare_method = (genericCompare word_sless (op=)),
+  compare_method = (genericCompare word_sless (=)),
 
   isLess_method = word_sless,
 
@@ -723,7 +722,7 @@ definition instance_Num_NumAbs_Num_int64_dict  :: "( 64 word)NumAbs_class "  whe
 definition instance_Num_NumAdd_Num_int64_dict  :: "( 64 word)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_int64_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val int64Minus : int64 -> int64 -> int64*)
@@ -731,7 +730,7 @@ definition instance_Num_NumAdd_Num_int64_dict  :: "( 64 word)NumAdd_class "  whe
 definition instance_Num_NumMinus_Num_int64_dict  :: "( 64 word)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_int64_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val int64Succ : int64 -> int64*)
@@ -754,7 +753,7 @@ definition instance_Num_NumPred_Num_int64_dict  :: "( 64 word)NumPred_class "  w
 definition instance_Num_NumMult_Num_int64_dict  :: "( 64 word)NumMult_class "  where 
      " instance_Num_NumMult_Num_int64_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 
@@ -763,7 +762,7 @@ definition instance_Num_NumMult_Num_int64_dict  :: "( 64 word)NumMult_class "  w
 definition instance_Num_NumPow_Num_int64_dict  :: "( 64 word)NumPow_class "  where 
      " instance_Num_NumPow_Num_int64_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val int64Div : int64 -> int64 -> int64*)
@@ -771,13 +770,13 @@ definition instance_Num_NumPow_Num_int64_dict  :: "( 64 word)NumPow_class "  whe
 definition instance_Num_NumIntegerDivision_Num_int64_dict  :: "( 64 word)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_Num_int64_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_Num_int64_dict  :: "( 64 word)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_int64_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val int64Mod : int64 -> int64 -> int64*)
@@ -785,7 +784,7 @@ definition instance_Num_NumDivision_Num_int64_dict  :: "( 64 word)NumDivision_cl
 definition instance_Num_NumRemainder_Num_int64_dict  :: "( 64 word)NumRemainder_class "  where 
      " instance_Num_NumRemainder_Num_int64_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 (*val int64Min : int64 -> int64 -> int64*)
@@ -821,15 +820,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_int64_dict  :: "( 64 word)OrdMax
 definition instance_Basic_classes_Ord_Num_integer_dict  :: "(int)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_integer_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val integerNegate : integer -> integer*)
@@ -853,7 +852,7 @@ definition instance_Num_NumAbs_Num_integer_dict  :: "(int)NumAbs_class "  where
 definition instance_Num_NumAdd_Num_integer_dict  :: "(int)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_integer_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val integerMinus : integer -> integer -> integer*)
@@ -861,7 +860,7 @@ definition instance_Num_NumAdd_Num_integer_dict  :: "(int)NumAdd_class "  where
 definition instance_Num_NumMinus_Num_integer_dict  :: "(int)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_integer_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val integerSucc : integer -> integer*)
@@ -883,7 +882,7 @@ definition instance_Num_NumPred_Num_integer_dict  :: "(int)NumPred_class "  wher
 definition instance_Num_NumMult_Num_integer_dict  :: "(int)NumMult_class "  where 
      " instance_Num_NumMult_Num_integer_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 
@@ -892,7 +891,7 @@ definition instance_Num_NumMult_Num_integer_dict  :: "(int)NumMult_class "  wher
 definition instance_Num_NumPow_Num_integer_dict  :: "(int)NumPow_class "  where 
      " instance_Num_NumPow_Num_integer_dict = ((|
 
-  numPow_method = (op^)|) )"
+  numPow_method = (^)|) )"
 
 
 (*val integerDiv : integer -> integer -> integer*)
@@ -900,13 +899,13 @@ definition instance_Num_NumPow_Num_integer_dict  :: "(int)NumPow_class "  where
 definition instance_Num_NumIntegerDivision_Num_integer_dict  :: "(int)NumIntegerDivision_class "  where 
      " instance_Num_NumIntegerDivision_Num_integer_dict = ((|
 
-  div_method = (op div)|) )"
+  div_method = (div)|) )"
 
 
 definition instance_Num_NumDivision_Num_integer_dict  :: "(int)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_integer_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val integerMod : integer -> integer -> integer*)
@@ -914,7 +913,7 @@ definition instance_Num_NumDivision_Num_integer_dict  :: "(int)NumDivision_class
 definition instance_Num_NumRemainder_Num_integer_dict  :: "(int)NumRemainder_class "  where 
      " instance_Num_NumRemainder_Num_integer_dict = ((|
 
-  mod_method = (op mod)|) )"
+  mod_method = (mod)|) )"
 
 
 (*val integerMin : integer -> integer -> integer*)
@@ -951,15 +950,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_integer_dict  :: "(int)OrdMaxMin
 definition instance_Basic_classes_Ord_Num_rational_dict  :: "(rat)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_rational_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val rationalAdd : rational -> rational -> rational*)
@@ -967,7 +966,7 @@ definition instance_Basic_classes_Ord_Num_rational_dict  :: "(rat)Ord_class "  w
 definition instance_Num_NumAdd_Num_rational_dict  :: "(rat)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_rational_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val rationalMinus : rational -> rational -> rational*)
@@ -975,7 +974,7 @@ definition instance_Num_NumAdd_Num_rational_dict  :: "(rat)NumAdd_class "  where
 definition instance_Num_NumMinus_Num_rational_dict  :: "(rat)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_rational_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val rationalNegate : rational -> rational*)
@@ -1013,7 +1012,7 @@ definition instance_Num_NumPred_Num_rational_dict  :: "(rat)NumPred_class "  whe
 definition instance_Num_NumMult_Num_rational_dict  :: "(rat)NumMult_class "  where 
      " instance_Num_NumMult_Num_rational_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 (*val rationalDiv : rational -> rational -> rational*)
@@ -1021,7 +1020,7 @@ definition instance_Num_NumMult_Num_rational_dict  :: "(rat)NumMult_class "  whe
 definition instance_Num_NumDivision_Num_rational_dict  :: "(rat)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_rational_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val rationalFromFrac : int -> int -> rational*)
@@ -1078,15 +1077,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_rational_dict  :: "(rat)OrdMaxMi
 definition instance_Basic_classes_Ord_Num_real_dict  :: "(real)Ord_class "  where 
      " instance_Basic_classes_Ord_Num_real_dict = ((|
 
-  compare_method = (genericCompare (op<) (op=)),
+  compare_method = (genericCompare (<) (=)),
 
-  isLess_method = (op<),
+  isLess_method = (<),
 
-  isLessEqual_method = (op \<le>),
+  isLessEqual_method = (\<le>),
 
-  isGreater_method = (op>),
+  isGreater_method = (>),
 
-  isGreaterEqual_method = (op \<ge>)|) )"
+  isGreaterEqual_method = (\<ge>)|) )"
 
 
 (*val realAdd : real -> real -> real*)
@@ -1094,7 +1093,7 @@ definition instance_Basic_classes_Ord_Num_real_dict  :: "(real)Ord_class "  wher
 definition instance_Num_NumAdd_Num_real_dict  :: "(real)NumAdd_class "  where 
      " instance_Num_NumAdd_Num_real_dict = ((|
 
-  numAdd_method = (op+)|) )"
+  numAdd_method = (+)|) )"
 
 
 (*val realMinus : real -> real -> real*)
@@ -1102,7 +1101,7 @@ definition instance_Num_NumAdd_Num_real_dict  :: "(real)NumAdd_class "  where
 definition instance_Num_NumMinus_Num_real_dict  :: "(real)NumMinus_class "  where 
      " instance_Num_NumMinus_Num_real_dict = ((|
 
-  numMinus_method = (op-)|) )"
+  numMinus_method = (-)|) )"
 
 
 (*val realNegate : real -> real*)
@@ -1140,7 +1139,7 @@ definition instance_Num_NumPred_Num_real_dict  :: "(real)NumPred_class "  where
 definition instance_Num_NumMult_Num_real_dict  :: "(real)NumMult_class "  where 
      " instance_Num_NumMult_Num_real_dict = ((|
 
-  numMult_method = (op*)|) )"
+  numMult_method = ( * )|) )"
 
 
 (*val realDiv : real -> real -> real*)
@@ -1148,7 +1147,7 @@ definition instance_Num_NumMult_Num_real_dict  :: "(real)NumMult_class "  where
 definition instance_Num_NumDivision_Num_real_dict  :: "(real)NumDivision_class "  where 
      " instance_Num_NumDivision_Num_real_dict = ((|
 
-  numDivision_method = (op div)|) )"
+  numDivision_method = (div)|) )"
 
 
 (*val realFromFrac : integer -> integer -> real*)
diff --git a/snapshots/isabelle/lib/lem/Lem_num_extra.thy b/snapshots/isabelle/lib/lem/Lem_num_extra.thy
index 0611862e..c1edb194 100644
--- a/snapshots/isabelle/lib/lem/Lem_num_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_num_extra.thy
@@ -1,11 +1,11 @@
-chapter \<open>Generated by Lem from num_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>num_extra.lem\<close>.\<close>
 
 theory "Lem_num_extra" 
 
-imports 
- 	 Main
-	 "Lem_num" 
-	 "Lem_string" 
+imports
+  Main
+  "Lem_num"
+  "Lem_string"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_pervasives.thy b/snapshots/isabelle/lib/lem/Lem_pervasives.thy
index 37da1224..b8f1ffd3 100644
--- a/snapshots/isabelle/lib/lem/Lem_pervasives.thy
+++ b/snapshots/isabelle/lib/lem/Lem_pervasives.thy
@@ -1,24 +1,24 @@
-chapter \<open>Generated by Lem from pervasives.lem.\<close>
+chapter \<open>Generated by Lem from \<open>pervasives.lem\<close>.\<close>
 
 theory "Lem_pervasives" 
 
-imports 
- 	 Main
-	 "Lem_basic_classes" 
-	 "Lem_bool" 
-	 "Lem_tuple" 
-	 "Lem_maybe" 
-	 "Lem_either" 
-	 "Lem_function" 
-	 "Lem_num" 
-	 "Lem_map" 
-	 "Lem_set" 
-	 "Lem_list" 
-	 "Lem_string" 
-	 "Lem_word" 
-	 "Lem_show" 
-	 "Lem_sorting" 
-	 "Lem_relation" 
+imports
+  Main
+  "Lem_basic_classes"
+  "Lem_bool"
+  "Lem_tuple"
+  "Lem_maybe"
+  "Lem_either"
+  "Lem_function"
+  "Lem_num"
+  "Lem_map"
+  "Lem_set"
+  "Lem_list"
+  "Lem_string"
+  "Lem_word"
+  "Lem_show"
+  "Lem_sorting"
+  "Lem_relation"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_pervasives_extra.thy b/snapshots/isabelle/lib/lem/Lem_pervasives_extra.thy
index 0e3e5a88..ba3ba259 100644
--- a/snapshots/isabelle/lib/lem/Lem_pervasives_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_pervasives_extra.thy
@@ -1,21 +1,21 @@
-chapter \<open>Generated by Lem from pervasives_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>pervasives_extra.lem\<close>.\<close>
 
 theory "Lem_pervasives_extra" 
 
-imports 
- 	 Main
-	 "Lem_pervasives" 
-	 "Lem_function_extra" 
-	 "Lem_maybe_extra" 
-	 "Lem_map_extra" 
-	 "Lem_num_extra" 
-	 "Lem_set_extra" 
-	 "Lem_set_helpers" 
-	 "Lem_list_extra" 
-	 "Lem_string_extra" 
-	 "Lem_assert_extra" 
-	 "Lem_show_extra" 
-	 "Lem_machine_word" 
+imports
+  Main
+  "Lem_pervasives"
+  "Lem_function_extra"
+  "Lem_maybe_extra"
+  "Lem_map_extra"
+  "Lem_num_extra"
+  "Lem_set_extra"
+  "Lem_set_helpers"
+  "Lem_list_extra"
+  "Lem_string_extra"
+  "Lem_assert_extra"
+  "Lem_show_extra"
+  "Lem_machine_word"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_relation.thy b/snapshots/isabelle/lib/lem/Lem_relation.thy
index 23e7d707..778507a7 100644
--- a/snapshots/isabelle/lib/lem/Lem_relation.thy
+++ b/snapshots/isabelle/lib/lem/Lem_relation.thy
@@ -1,14 +1,14 @@
-chapter \<open>Generated by Lem from relation.lem.\<close>
+chapter \<open>Generated by Lem from \<open>relation.lem\<close>.\<close>
 
 theory "Lem_relation" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_tuple" 
-	 "Lem_set" 
-	 "Lem_num" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_tuple"
+  "Lem_set"
+  "Lem_num"
 
 begin 
 
@@ -85,7 +85,7 @@ definition relFromPred  :: " 'a set \<Rightarrow> 'b set \<Rightarrow>('a \<Righ
 
 (*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*)
 definition relIdOn  :: " 'a set \<Rightarrow>('a*'a)set "  where 
-     " relIdOn s = ( relFromPred s s (op=))"
+     " relIdOn s = ( relFromPred s s (=))"
 
 
 (*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*)
diff --git a/snapshots/isabelle/lib/lem/Lem_set.thy b/snapshots/isabelle/lib/lem/Lem_set.thy
index f77d4d98..ab6ee68c 100644
--- a/snapshots/isabelle/lib/lem/Lem_set.thy
+++ b/snapshots/isabelle/lib/lem/Lem_set.thy
@@ -1,17 +1,17 @@
-chapter \<open>Generated by Lem from set.lem.\<close>
+chapter \<open>Generated by Lem from \<open>set.lem\<close>.\<close>
 
 theory "Lem_set" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_maybe" 
-	 "Lem_function" 
-	 "Lem_num" 
-	 "Lem_list" 
-	 "Lem_set_helpers" 
-	 "Lem" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_maybe"
+  "Lem_function"
+  "Lem_num"
+  "Lem_list"
+  "Lem_set_helpers"
+  "Lem"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_set_extra.thy b/snapshots/isabelle/lib/lem/Lem_set_extra.thy
index 33516be7..87ccacef 100644
--- a/snapshots/isabelle/lib/lem/Lem_set_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_set_extra.thy
@@ -1,17 +1,17 @@
-chapter \<open>Generated by Lem from set_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>set_extra.lem\<close>.\<close>
 
 theory "Lem_set_extra" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_maybe" 
-	 "Lem_function" 
-	 "Lem_num" 
-	 "Lem_list" 
-	 "Lem_sorting" 
-	 "Lem_set" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_maybe"
+  "Lem_function"
+  "Lem_num"
+  "Lem_list"
+  "Lem_sorting"
+  "Lem_set"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_set_helpers.thy b/snapshots/isabelle/lib/lem/Lem_set_helpers.thy
index 1a2f5f50..3b8991cf 100644
--- a/snapshots/isabelle/lib/lem/Lem_set_helpers.thy
+++ b/snapshots/isabelle/lib/lem/Lem_set_helpers.thy
@@ -1,14 +1,14 @@
-chapter \<open>Generated by Lem from set_helpers.lem.\<close>
+chapter \<open>Generated by Lem from \<open>set_helpers.lem\<close>.\<close>
 
 theory "Lem_set_helpers" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_maybe" 
-	 "Lem_function" 
-	 "Lem_num" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_maybe"
+  "Lem_function"
+  "Lem_num"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_show.thy b/snapshots/isabelle/lib/lem/Lem_show.thy
index fced534d..b55de519 100644
--- a/snapshots/isabelle/lib/lem/Lem_show.thy
+++ b/snapshots/isabelle/lib/lem/Lem_show.thy
@@ -1,13 +1,13 @@
-chapter \<open>Generated by Lem from show.lem.\<close>
+chapter \<open>Generated by Lem from \<open>show.lem\<close>.\<close>
 
 theory "Lem_show" 
 
-imports 
- 	 Main
-	 "Lem_string" 
-	 "Lem_maybe" 
-	 "Lem_num" 
-	 "Lem_basic_classes" 
+imports
+  Main
+  "Lem_string"
+  "Lem_maybe"
+  "Lem_num"
+  "Lem_basic_classes"
 
 begin 
 
@@ -26,7 +26,7 @@ record 'a Show_class=
 definition instance_Show_Show_string_dict  :: "(string)Show_class "  where 
      " instance_Show_Show_string_dict = ((|
 
-  show_method = (\<lambda> s. ([(char_of_nat 34)]) @ (s @ ([(char_of_nat 34)])))|) )"
+  show_method = (\<lambda> s. ([(CHR 0x27)]) @ (s @ ([(CHR 0x27)])))|) )"
 
 
 (*val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string*)
diff --git a/snapshots/isabelle/lib/lem/Lem_show_extra.thy b/snapshots/isabelle/lib/lem/Lem_show_extra.thy
index 25ab2570..36e23aca 100644
--- a/snapshots/isabelle/lib/lem/Lem_show_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_show_extra.thy
@@ -1,18 +1,18 @@
-chapter \<open>Generated by Lem from show_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>show_extra.lem\<close>.\<close>
 
 theory "Lem_show_extra" 
 
-imports 
- 	 Main
-	 "Lem_string" 
-	 "Lem_maybe" 
-	 "Lem_num" 
-	 "Lem_basic_classes" 
-	 "Lem_set" 
-	 "Lem_relation" 
-	 "Lem_show" 
-	 "Lem_set_extra" 
-	 "Lem_string_extra" 
+imports
+  Main
+  "Lem_string"
+  "Lem_maybe"
+  "Lem_num"
+  "Lem_basic_classes"
+  "Lem_set"
+  "Lem_relation"
+  "Lem_show"
+  "Lem_set_extra"
+  "Lem_string_extra"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_sorting.thy b/snapshots/isabelle/lib/lem/Lem_sorting.thy
index d42425a2..48032c8e 100644
--- a/snapshots/isabelle/lib/lem/Lem_sorting.thy
+++ b/snapshots/isabelle/lib/lem/Lem_sorting.thy
@@ -1,16 +1,16 @@
-chapter \<open>Generated by Lem from sorting.lem.\<close>
+chapter \<open>Generated by Lem from \<open>sorting.lem\<close>.\<close>
 
 theory "Lem_sorting" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_maybe" 
-	 "Lem_list" 
-	 "Lem_num" 
-	 "Lem" 
-	 "~~/src/HOL/Library/Permutation" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_maybe"
+  "Lem_list"
+  "Lem_num"
+  "Lem"
+  "HOL-Library.Permutation"
 
 begin 
 
@@ -18,7 +18,7 @@ begin
 
 (*open import Bool Basic_classes Maybe List Num*)
 
-(*open import {isabelle} `~~/src/HOL/Library/Permutation`*)
+(*open import {isabelle} `HOL-Library.Permutation`*)
 (*open import {coq} `Coq.Lists.List`*)
 (*open import {hol} `sortingTheory` `permLib`*)
 (*open import {isabelle} `$LIB_DIR/Lem`*)
diff --git a/snapshots/isabelle/lib/lem/Lem_string.thy b/snapshots/isabelle/lib/lem/Lem_string.thy
index 9df246c4..7fd329bd 100644
--- a/snapshots/isabelle/lib/lem/Lem_string.thy
+++ b/snapshots/isabelle/lib/lem/Lem_string.thy
@@ -1,12 +1,12 @@
-chapter \<open>Generated by Lem from string.lem.\<close>
+chapter \<open>Generated by Lem from \<open>string.lem\<close>.\<close>
 
 theory "Lem_string" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
-	 "Lem_list" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
+  "Lem_list"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_string_extra.thy b/snapshots/isabelle/lib/lem/Lem_string_extra.thy
index bd8317ba..9991308f 100644
--- a/snapshots/isabelle/lib/lem/Lem_string_extra.thy
+++ b/snapshots/isabelle/lib/lem/Lem_string_extra.thy
@@ -1,14 +1,14 @@
-chapter \<open>Generated by Lem from string_extra.lem.\<close>
+chapter \<open>Generated by Lem from \<open>string_extra.lem\<close>.\<close>
 
 theory "Lem_string_extra" 
 
-imports 
- 	 Main
-	 "Lem_num" 
-	 "Lem_list" 
-	 "Lem_basic_classes" 
-	 "Lem_string" 
-	 "Lem_list_extra" 
+imports
+  Main
+  "Lem_num"
+  "Lem_list"
+  "Lem_basic_classes"
+  "Lem_string"
+  "Lem_list_extra"
 
 begin 
 
@@ -43,7 +43,7 @@ fun  stringFromNatHelper  :: " nat \<Rightarrow>(char)list \<Rightarrow>(char)li
   if n =( 0 :: nat) then
     acc1
   else
-    stringFromNatHelper (n div( 10 :: nat)) (char_of_nat ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))"
+    stringFromNatHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))"
 
 
 (*val stringFromNat : nat -> string*)
@@ -58,7 +58,7 @@ fun  stringFromNaturalHelper  :: " nat \<Rightarrow>(char)list \<Rightarrow>(cha
   if n =( 0 :: nat) then
     acc1
   else
-    stringFromNaturalHelper (n div( 10 :: nat)) (char_of_nat ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))"
+    stringFromNaturalHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))"
 
 
 (*val stringFromNatural : natural -> string*)
@@ -98,7 +98,7 @@ definition nth  :: " string \<Rightarrow> nat \<Rightarrow> char "  where
 (*val stringConcat : list string -> string*)
 definition stringConcat  :: "(string)list \<Rightarrow> string "  where 
      " stringConcat s = (
-  List.foldr (op@) s (''''))"
+  List.foldr (@) s (''''))"
 
 
 (******************************************************************************)
diff --git a/snapshots/isabelle/lib/lem/Lem_tuple.thy b/snapshots/isabelle/lib/lem/Lem_tuple.thy
index 66f1a209..292dc17a 100644
--- a/snapshots/isabelle/lib/lem/Lem_tuple.thy
+++ b/snapshots/isabelle/lib/lem/Lem_tuple.thy
@@ -1,11 +1,11 @@
-chapter \<open>Generated by Lem from tuple.lem.\<close>
+chapter \<open>Generated by Lem from \<open>tuple.lem\<close>.\<close>
 
 theory "Lem_tuple" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_basic_classes" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_basic_classes"
 
 begin 
 
diff --git a/snapshots/isabelle/lib/lem/Lem_word.thy b/snapshots/isabelle/lib/lem/Lem_word.thy
index bc56da3c..af0ef53a 100644
--- a/snapshots/isabelle/lib/lem/Lem_word.thy
+++ b/snapshots/isabelle/lib/lem/Lem_word.thy
@@ -1,15 +1,15 @@
-chapter \<open>Generated by Lem from word.lem.\<close>
+chapter \<open>Generated by Lem from \<open>word.lem\<close>.\<close>
 
 theory "Lem_word" 
 
-imports 
- 	 Main
-	 "Lem_bool" 
-	 "Lem_maybe" 
-	 "Lem_num" 
-	 "Lem_basic_classes" 
-	 "Lem_list" 
-	 "~~/src/HOL/Word/Word" 
+imports
+  Main
+  "Lem_bool"
+  "Lem_maybe"
+  "Lem_num"
+  "Lem_basic_classes"
+  "Lem_list"
+  "HOL-Word.Word"
 
 begin 
 
@@ -17,7 +17,7 @@ begin
 
 (*open import Bool Maybe Num Basic_classes List*)
 
-(*open import {isabelle} `~~/src/HOL/Word/Word`*)
+(*open import {isabelle} `HOL-Word.Word`*)
 (*open import {hol} `wordsTheory` `wordsLib`*)
 
 
@@ -62,8 +62,8 @@ definition bitSeqFromBoolList  :: "(bool)list \<Rightarrow>(bitSequence)option "
 (*val cleanBitSeq : bitSequence -> bitSequence*)
 fun cleanBitSeq  :: " bitSequence \<Rightarrow> bitSequence "  where 
      " cleanBitSeq (BitSeq len s bl) = ( (case  len of
-    None => (BitSeq len s (List.rev (dropWhile ((op \<longleftrightarrow>) s) (List.rev bl))))
-  | Some n  => (BitSeq len s (List.rev (dropWhile ((op \<longleftrightarrow>) s) (List.rev (List.take (n-( 1 :: nat)) bl)))))
+    None => (BitSeq len s (List.rev (dropWhile ((\<longleftrightarrow>) s) (List.rev bl))))
+  | Some n  => (BitSeq len s (List.rev (dropWhile ((\<longleftrightarrow>) s) (List.rev (List.take (n-( 1 :: nat)) bl)))))
 ))"
 
 
@@ -143,10 +143,10 @@ definition bitSeqBinop  :: "(bool \<Rightarrow> bool \<Rightarrow> bool)\<Righta
 
 
 definition bitSeqAnd  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqAnd = ( bitSeqBinop (op \<and>))"
+     " bitSeqAnd = ( bitSeqBinop (\<and>))"
 
 definition bitSeqOr  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqOr = ( bitSeqBinop (op \<or>))"
+     " bitSeqOr = ( bitSeqBinop (\<or>))"
 
 definition bitSeqXor  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
      " bitSeqXor = ( bitSeqBinop (\<lambda> b1 b2. \<not> (b1 \<longleftrightarrow> b2)))"
@@ -277,27 +277,27 @@ definition bitSeqArithBinTest  :: "(int \<Rightarrow> int \<Rightarrow> 'a)\<Rig
 
 (*val bitSeqLess : bitSequence -> bitSequence -> bool*)
 definition bitSeqLess  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bool "  where 
-     " bitSeqLess bs1 bs2 = ( bitSeqArithBinTest (op<) bs1 bs2 )"
+     " bitSeqLess bs1 bs2 = ( bitSeqArithBinTest (<) bs1 bs2 )"
 
 
 (*val bitSeqLessEqual : bitSequence -> bitSequence -> bool*)
 definition bitSeqLessEqual  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bool "  where 
-     " bitSeqLessEqual bs1 bs2 = ( bitSeqArithBinTest (op \<le>) bs1 bs2 )"
+     " bitSeqLessEqual bs1 bs2 = ( bitSeqArithBinTest (\<le>) bs1 bs2 )"
 
 
 (*val bitSeqGreater : bitSequence -> bitSequence -> bool*)
 definition bitSeqGreater  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bool "  where 
-     " bitSeqGreater bs1 bs2 = ( bitSeqArithBinTest (op>) bs1 bs2 )"
+     " bitSeqGreater bs1 bs2 = ( bitSeqArithBinTest (>) bs1 bs2 )"
 
 
 (*val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool*)
 definition bitSeqGreaterEqual  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bool "  where 
-     " bitSeqGreaterEqual bs1 bs2 = ( bitSeqArithBinTest (op \<ge>) bs1 bs2 )"
+     " bitSeqGreaterEqual bs1 bs2 = ( bitSeqArithBinTest (\<ge>) bs1 bs2 )"
 
 
 (*val bitSeqCompare : bitSequence -> bitSequence -> ordering*)
 definition bitSeqCompare  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> ordering "  where 
-     " bitSeqCompare bs1 bs2 = ( bitSeqArithBinTest (genericCompare (op<) (op=)) bs1 bs2 )"
+     " bitSeqCompare bs1 bs2 = ( bitSeqArithBinTest (genericCompare (<) (=)) bs1 bs2 )"
 
 
 definition instance_Basic_classes_Ord_Word_bitSequence_dict  :: "(bitSequence)Ord_class "  where 
@@ -329,7 +329,7 @@ definition instance_Num_NumNegate_Word_bitSequence_dict  :: "(bitSequence)NumNeg
 
 (*val bitSeqAdd : bitSequence -> bitSequence -> bitSequence*)
 definition bitSeqAdd  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqAdd bs1 bs2 = ( bitSeqArithBinOp (op+) bs1 bs2 )"
+     " bitSeqAdd bs1 bs2 = ( bitSeqArithBinOp (+) bs1 bs2 )"
 
 
 definition instance_Num_NumAdd_Word_bitSequence_dict  :: "(bitSequence)NumAdd_class "  where 
@@ -340,7 +340,7 @@ definition instance_Num_NumAdd_Word_bitSequence_dict  :: "(bitSequence)NumAdd_cl
 
 (*val bitSeqMinus : bitSequence -> bitSequence -> bitSequence*)
 definition bitSeqMinus  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqMinus bs1 bs2 = ( bitSeqArithBinOp (op-) bs1 bs2 )"
+     " bitSeqMinus bs1 bs2 = ( bitSeqArithBinOp (-) bs1 bs2 )"
 
 
 definition instance_Num_NumMinus_Word_bitSequence_dict  :: "(bitSequence)NumMinus_class "  where 
@@ -373,7 +373,7 @@ definition instance_Num_NumPred_Word_bitSequence_dict  :: "(bitSequence)NumPred_
 
 (*val bitSeqMult : bitSequence -> bitSequence -> bitSequence*)
 definition bitSeqMult  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqMult bs1 bs2 = ( bitSeqArithBinOp (op*) bs1 bs2 )"
+     " bitSeqMult bs1 bs2 = ( bitSeqArithBinOp ( * ) bs1 bs2 )"
 
 
 definition instance_Num_NumMult_Word_bitSequence_dict  :: "(bitSequence)NumMult_class "  where 
@@ -396,7 +396,7 @@ definition instance_Num_NumPow_Word_bitSequence_dict  :: "(bitSequence)NumPow_cl
 
 (*val bitSeqDiv : bitSequence -> bitSequence -> bitSequence*)
 definition bitSeqDiv  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqDiv bs1 bs2 = ( bitSeqArithBinOp (op div) bs1 bs2 )"
+     " bitSeqDiv bs1 bs2 = ( bitSeqArithBinOp (div) bs1 bs2 )"
 
 
 definition instance_Num_NumIntegerDivision_Word_bitSequence_dict  :: "(bitSequence)NumIntegerDivision_class "  where 
@@ -413,7 +413,7 @@ definition instance_Num_NumDivision_Word_bitSequence_dict  :: "(bitSequence)NumD
 
 (*val bitSeqMod : bitSequence -> bitSequence -> bitSequence*)
 definition bitSeqMod  :: " bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence "  where 
-     " bitSeqMod bs1 bs2 = ( bitSeqArithBinOp (op mod) bs1 bs2 )"
+     " bitSeqMod bs1 bs2 = ( bitSeqArithBinOp (mod) bs1 bs2 )"
 
 
 definition instance_Num_NumRemainder_Word_bitSequence_dict  :: "(bitSequence)NumRemainder_class "  where 
@@ -555,7 +555,7 @@ definition instance_Word_WordNot_Num_int32_dict  :: "( 32 word)WordNot_class "
 definition instance_Word_WordOr_Num_int32_dict  :: "( 32 word)WordOr_class "  where 
      " instance_Word_WordOr_Num_int32_dict = ((|
 
-  lor_method = (op OR)|) )"
+  lor_method = (OR)|) )"
 
 
 (*val int32Lxor : int32 -> int32 -> int32*) (* XXX: fix *)
@@ -563,7 +563,7 @@ definition instance_Word_WordOr_Num_int32_dict  :: "( 32 word)WordOr_class "  wh
 definition instance_Word_WordXor_Num_int32_dict  :: "( 32 word)WordXor_class "  where 
      " instance_Word_WordXor_Num_int32_dict = ((|
 
-  lxor_method = (op XOR)|) )"
+  lxor_method = (XOR)|) )"
 
 
 (*val int32Land : int32 -> int32 -> int32*) (* XXX: fix *)
@@ -571,7 +571,7 @@ definition instance_Word_WordXor_Num_int32_dict  :: "( 32 word)WordXor_class "
 definition instance_Word_WordAnd_Num_int32_dict  :: "( 32 word)WordAnd_class "  where 
      " instance_Word_WordAnd_Num_int32_dict = ((|
 
-  land_method = (op AND)|) )"
+  land_method = (AND)|) )"
 
 
 (*val int32Lsl  : int32 -> nat -> int32*) (* XXX: fix *)
@@ -579,7 +579,7 @@ definition instance_Word_WordAnd_Num_int32_dict  :: "( 32 word)WordAnd_class "
 definition instance_Word_WordLsl_Num_int32_dict  :: "( 32 word)WordLsl_class "  where 
      " instance_Word_WordLsl_Num_int32_dict = ((|
 
-  lsl_method = (op<<)|) )"
+  lsl_method = (<<)|) )"
 
 
 (*val int32Lsr  : int32 -> nat -> int32*) (* XXX: fix *)
@@ -587,7 +587,7 @@ definition instance_Word_WordLsl_Num_int32_dict  :: "( 32 word)WordLsl_class "
 definition instance_Word_WordLsr_Num_int32_dict  :: "( 32 word)WordLsr_class "  where 
      " instance_Word_WordLsr_Num_int32_dict = ((|
 
-  lsr_method = (op>>)|) )"
+  lsr_method = (>>)|) )"
 
 
 
@@ -596,7 +596,7 @@ definition instance_Word_WordLsr_Num_int32_dict  :: "( 32 word)WordLsr_class "
 definition instance_Word_WordAsr_Num_int32_dict  :: "( 32 word)WordAsr_class "  where 
      " instance_Word_WordAsr_Num_int32_dict = ((|
 
-  asr_method = (op>>>)|) )"
+  asr_method = (>>>)|) )"
 
 
 
@@ -617,7 +617,7 @@ definition instance_Word_WordNot_Num_int64_dict  :: "( 64 word)WordNot_class "
 definition instance_Word_WordOr_Num_int64_dict  :: "( 64 word)WordOr_class "  where 
      " instance_Word_WordOr_Num_int64_dict = ((|
 
-  lor_method = (op OR)|) )"
+  lor_method = (OR)|) )"
 
 
 (*val int64Lxor : int64 -> int64 -> int64*) (* XXX: fix *)
@@ -625,7 +625,7 @@ definition instance_Word_WordOr_Num_int64_dict  :: "( 64 word)WordOr_class "  wh
 definition instance_Word_WordXor_Num_int64_dict  :: "( 64 word)WordXor_class "  where 
      " instance_Word_WordXor_Num_int64_dict = ((|
 
-  lxor_method = (op XOR)|) )"
+  lxor_method = (XOR)|) )"
 
 
 (*val int64Land : int64 -> int64 -> int64*) (* XXX: fix *)
@@ -633,7 +633,7 @@ definition instance_Word_WordXor_Num_int64_dict  :: "( 64 word)WordXor_class "
 definition instance_Word_WordAnd_Num_int64_dict  :: "( 64 word)WordAnd_class "  where 
      " instance_Word_WordAnd_Num_int64_dict = ((|
 
-  land_method = (op AND)|) )"
+  land_method = (AND)|) )"
 
 
 (*val int64Lsl  : int64 -> nat -> int64*) (* XXX: fix *)
@@ -641,7 +641,7 @@ definition instance_Word_WordAnd_Num_int64_dict  :: "( 64 word)WordAnd_class "
 definition instance_Word_WordLsl_Num_int64_dict  :: "( 64 word)WordLsl_class "  where 
      " instance_Word_WordLsl_Num_int64_dict = ((|
 
-  lsl_method = (op<<)|) )"
+  lsl_method = (<<)|) )"
 
 
 (*val int64Lsr  : int64 -> nat -> int64*) (* XXX: fix *)
@@ -649,7 +649,7 @@ definition instance_Word_WordLsl_Num_int64_dict  :: "( 64 word)WordLsl_class "
 definition instance_Word_WordLsr_Num_int64_dict  :: "( 64 word)WordLsr_class "  where 
      " instance_Word_WordLsr_Num_int64_dict = ((|
 
-  lsr_method = (op>>)|) )"
+  lsr_method = (>>)|) )"
 
 
 (*val int64Asr  : int64 -> nat -> int64*) (* XXX: fix *)
@@ -657,7 +657,7 @@ definition instance_Word_WordLsr_Num_int64_dict  :: "( 64 word)WordLsr_class "
 definition instance_Word_WordAsr_Num_int64_dict  :: "( 64 word)WordAsr_class "  where 
      " instance_Word_WordAsr_Num_int64_dict = ((|
 
-  asr_method = (op>>>)|) )"
+  asr_method = (>>>)|) )"