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/ZF/ArithSimp.thy
changeset 13611 2edf034c902a
parent 13356 c9cfe1638bf2
child 13615 449a70d88b38 
--- a/src/ZF/ArithSimp.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/ArithSimp.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -119,7 +119,7 @@
      "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (rule raw_mod_def [THEN def_transrec, THEN trans])
-apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
+apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
 done
 
 
@@ -160,7 +160,7 @@
 prefer 2 apply blast
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (rule raw_div_def [THEN def_transrec, THEN trans])
-apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
+apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
 done
 
 lemma div_geq [simp]:
isabelle