Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Complex/hcomplex_arith.ML
changeset 14335 9c0b5e081037
parent 14326 c817dd885a32 
--- a/src/HOL/Complex/hcomplex_arith.ML	Thu Jan 01 10:06:32 2004 +0100
+++ b/src/HOL/Complex/hcomplex_arith.ML	Thu Jan 01 21:47:07 2004 +0100
@@ -19,7 +19,7 @@
   val trans_tac         = Real_Numeral_Simprocs.trans_tac
   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s))
                  THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac))
+                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
   val numeral_simp_tac	= 
          ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
@@ -107,7 +107,7 @@
   val dest_coeff	= dest_coeff
   val find_first	= find_first []
   val trans_tac         = Real_Numeral_Simprocs.trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac))
+  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
   end;
isabelle