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/Reflection.thy
changeset 13268 240509babf00
parent 13223 45be08fbdcff
child 13292 f504f5d284d3 
--- a/src/ZF/Constructible/Reflection.thy	Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/Reflection.thy	Mon Jul 01 18:16:18 2002 +0200
@@ -55,7 +55,7 @@
 
 theorem (in reflection) Not_reflection [intro]:
      "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
-by (simp add: Reflects_def); 
+by (simp add: Reflects_def) 
 
 theorem (in reflection) And_reflection [intro]:
      "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
isabelle