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 13615 449a70d88b38
parent 13611 2edf034c902a
child 13628 87482b5e3f2e 
--- a/src/ZF/Constructible/Relative.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -1203,7 +1203,6 @@
 lemma (in M_basic) restriction_is_function: 
      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
       ==> function(z)"
-apply (rotate_tac 1)
 apply (simp add: restriction_def ball_iff_equiv) 
 apply (unfold function_def, blast) 
 done
isabelle