--- 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"
--- 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
--- 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 [])"
--- 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"];
-
--- 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.
--- 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
-