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/HOL/TLA/TLA.thy
changeset 9517 f58863b1406a
parent 7562 8519d5019309
child 12114 a8e860c86252 
--- a/src/HOL/TLA/TLA.thy	Thu Aug 03 19:28:37 2000 +0200
+++ b/src/HOL/TLA/TLA.thy	Thu Aug 03 19:29:03 2000 +0200
@@ -81,7 +81,7 @@
   primeI     "|- []P --> Init P`"
   primeE     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
   indT       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
-  allT       "|- (! x. [](F x)) = ([](! x. F x))"
+  allT       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
 
   necT       "|- F ==> |- []F"      (* polymorphic *)
isabelle