src/ZF/Constructible/Relative.thy
changeset 13611 2edf034c902a
parent 13564 1500a2e48d44
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:44:00 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:47:03 2002 +0200
     1.3 @@ -967,7 +967,7 @@
     1.4  apply (simp add: powerset_def) 
     1.5  apply (rule equalityI, clarify, simp)
     1.6   apply (frule transM, assumption) 
     1.7 - apply (frule transM, assumption, simp) 
     1.8 + apply (frule transM, assumption, simp (no_asm_simp))
     1.9   apply blast 
    1.10  apply clarify
    1.11  apply (frule transM, assumption, force)