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/Sequents/LK.thy
changeset 3839 56544d061e1d
parent 2073 fb0655539d05
child 6456 23602e214ebf 
--- a/src/Sequents/LK.thy	Fri Oct 10 17:38:50 1997 +0200
+++ b/src/Sequents/LK.thy	Fri Oct 10 18:17:17 1997 +0200
@@ -59,11 +59,11 @@
 
   (*Quantifiers*)
 
-  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
-  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
+  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
+  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
 
-  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
-  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
+  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
+  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
 
   (*Equality*)
 
@@ -75,7 +75,7 @@
   (*Descriptions*)
 
   The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
-          $H |- $E, P(THE x.P(x)), $F"
+          $H |- $E, P(THE x. P(x)), $F"
 end
 
   ML
isabelle