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/Constructible/Relative.thy
changeset 13611 2edf034c902a
parent 13564 1500a2e48d44
child 13615 449a70d88b38 
--- a/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -967,7 +967,7 @@
 apply (simp add: powerset_def) 
 apply (rule equalityI, clarify, simp)
  apply (frule transM, assumption) 
- apply (frule transM, assumption, simp) 
+ apply (frule transM, assumption, simp (no_asm_simp))
  apply blast 
 apply clarify
 apply (frule transM, assumption, force)
isabelle