diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -118,7 +118,7 @@
 lemma mult_raw_rsp[quotient_rsp]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(auto)
-apply(simp add: mult algebra_simps)
+apply(simp add: algebra_simps)
 sorry
 
 lemma le_raw_rsp[quotient_rsp]:
@@ -144,11 +144,11 @@
 lemma mult_assoc_raw:
   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 by (cases i, cases j, cases k) 
-   (simp add: mult algebra_simps)
+   (simp add: algebra_simps)
 
 lemma mult_sym_raw:
   shows "mult_raw i j \<approx> mult_raw j i"
-by (cases i, cases j) (simp)
+by (cases i, cases j) (simp add: algebra_simps)
 
 lemma mult_one_raw:
   shows "mult_raw  (1, 0) i \<approx> i"
@@ -157,7 +157,7 @@
 lemma mult_plus_comm_raw:
   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 by (cases i, cases j, cases k) 
-   (simp add: mult algebra_simps)
+   (simp add: algebra_simps)
 
 lemma one_zero_distinct:
   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
@@ -297,7 +297,7 @@
   "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
 apply(cases i, cases j, cases k)
-apply(auto simp add: mult algebra_simps)
+apply(auto simp add: algebra_simps)
 sorry
 
 
@@ -383,13 +383,13 @@
 class number = -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
-use "~~/src/HOL/Tools/numeral.ML"
+(*use "~~/src/HOL/Tools/numeral.ML"
 
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 use "~~/src/HOL/Tools/numeral_syntax.ML"
-(*
+
 setup NumeralSyntax.setup
 
 abbreviation
@@ -433,4 +433,4 @@
 
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
-*)
\ No newline at end of file
+*)