# HG changeset patch
# User wenzelm
# Date 1265920310 -3600
# Node ID e384e27c229fd5dae86186bc9ea5ab42acaf233b
# Parent  bdca9f765ee4d6181b1129ff8caee54c24741f68
modernized syntax/translations;
tuned headers;

diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/Action.thy	Thu Feb 11 21:31:50 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Action.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Action.thy 
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* The action level of TLA as an Isabelle theory *}
@@ -50,13 +48,13 @@
 
 translations
   "ACT A"            =>   "(A::state*state => _)"
-  "_before"          ==   "before"
-  "_after"           ==   "after"
+  "_before"          ==   "CONST before"
+  "_after"           ==   "CONST after"
   "_prime"           =>   "_after"
-  "_unchanged"       ==   "unch"
-  "_SqAct"           ==   "SqAct"
-  "_AnAct"           ==   "AnAct"
-  "_Enabled"         ==   "enabled"
+  "_unchanged"       ==   "CONST unch"
+  "_SqAct"           ==   "CONST SqAct"
+  "_AnAct"           ==   "CONST AnAct"
+  "_Enabled"         ==   "CONST enabled"
   "w |= [A]_v"       <=   "_SqAct A v w"
   "w |= <A>_v"       <=   "_AnAct A v w"
   "s |= Enabled A"   <=   "_Enabled A s"
diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/Init.thy	Thu Feb 11 21:31:50 2010 +0100
@@ -1,11 +1,10 @@
-(*
-    File:        TLA/Init.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Init.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 
-Introduces type of temporal formulas. Defines interface between
-temporal formulas and its "subformulas" (state predicates and actions).
+Introduces type of temporal formulas.  Defines interface between
+temporal formulas and its "subformulas" (state predicates and
+actions).
 *)
 
 theory Init
@@ -26,12 +25,12 @@
   st2         :: "behavior => state"
 
 syntax
-  TEMP       :: "lift => 'a"                          ("(TEMP _)")
+  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
   "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
 
 translations
   "TEMP F"   => "(F::behavior => _)"
-  "_Init"    == "Initial"
+  "_Init"    == "CONST Initial"
   "sigma |= Init F"  <= "_Init F sigma"
 
 defs
diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy	Thu Feb 11 21:31:50 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Intensional.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Intensional.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* A framework for "intensional" (possible-world based) logics
@@ -95,11 +93,11 @@
   "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
 
 translations
-  "_const"        == "const"
-  "_lift"         == "lift"
-  "_lift2"        == "lift2"
-  "_lift3"        == "lift3"
-  "_Valid"        == "Valid"
+  "_const"        == "CONST const"
+  "_lift"         == "CONST lift"
+  "_lift2"        == "CONST lift2"
+  "_lift3"        == "CONST lift3"
+  "_Valid"        == "CONST Valid"
   "_RAll x A"     == "Rall x. A"
   "_REx x  A"     == "Rex x. A"
   "_REx1 x  A"    == "Rex! x. A"
@@ -112,11 +110,11 @@
 
   "_liftEqu"      == "_lift2 (op =)"
   "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
-  "_liftNot"      == "_lift Not"
+  "_liftNot"      == "_lift (CONST Not)"
   "_liftAnd"      == "_lift2 (op &)"
   "_liftOr"       == "_lift2 (op | )"
   "_liftImp"      == "_lift2 (op -->)"
-  "_liftIf"       == "_lift3 If"
+  "_liftIf"       == "_lift3 (CONST If)"
   "_liftPlus"     == "_lift2 (op +)"
   "_liftMinus"    == "_lift2 (op -)"
   "_liftTimes"    == "_lift2 (op *)"
@@ -126,12 +124,12 @@
   "_liftLeq"      == "_lift2 (op <=)"
   "_liftMem"      == "_lift2 (op :)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
-  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
-  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
+  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
+  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
-  "_liftPair"     == "_lift2 Pair"
-  "_liftCons"     == "lift2 Cons"
-  "_liftApp"      == "lift2 (op @)"
+  "_liftPair"     == "_lift2 (CONST Pair)"
+  "_liftCons"     == "CONST lift2 (CONST Cons)"
+  "_liftApp"      == "CONST lift2 (op @)"
   "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   "_liftList x"   == "_liftCons x (_const [])"
 
diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/ROOT.ML	Thu Feb 11 21:31:50 2010 +0100
@@ -1,7 +1,3 @@
-(*  Title:      HOL/TLA/ROOT.ML
-
-Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
-*)
+(* The Temporal Logic of Actions *)
 
 use_thys ["TLA"];
-
diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/Stfun.thy	Thu Feb 11 21:31:50 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Stfun.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Stfun.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* States and state functions for TLA as an "intensional" logic *}
@@ -42,7 +40,7 @@
 
 translations
   "PRED P"   =>  "(P::state => _)"
-  "_stvars"  ==  "stvars"
+  "_stvars"  ==  "CONST stvars"
 
 defs
   (* Base variables may be assigned arbitrary (type-correct) values.
diff -r bdca9f765ee4 -r e384e27c229f src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Thu Feb 11 13:54:53 2010 +0100
+++ b/src/HOL/TLA/TLA.thy	Thu Feb 11 21:31:50 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/TLA.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/TLA.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* The temporal level of TLA *}
@@ -1168,4 +1166,3 @@
   done
 
 end
-