modernized syntax/translations;
authorwenzelm
Thu Feb 11 21:31:50 2010 +0100 (2010-02-11)
changeset 35108e384e27c229f
parent 35107 bdca9f765ee4
child 35109 0015a0a99ae9
modernized syntax/translations;
tuned headers;
src/HOL/TLA/Action.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/ROOT.ML
src/HOL/TLA/Stfun.thy
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Thu Feb 11 13:54:53 2010 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Thu Feb 11 21:31:50 2010 +0100
     1.3 @@ -1,8 +1,6 @@
     1.4 -(*
     1.5 -    File:        TLA/Action.thy
     1.6 -    ID:          $Id$
     1.7 -    Author:      Stephan Merz
     1.8 -    Copyright:   1998 University of Munich
     1.9 +(*  Title:      HOL/TLA/Action.thy 
    1.10 +    Author:     Stephan Merz
    1.11 +    Copyright:  1998 University of Munich
    1.12  *)
    1.13  
    1.14  header {* The action level of TLA as an Isabelle theory *}
    1.15 @@ -50,13 +48,13 @@
    1.16  
    1.17  translations
    1.18    "ACT A"            =>   "(A::state*state => _)"
    1.19 -  "_before"          ==   "before"
    1.20 -  "_after"           ==   "after"
    1.21 +  "_before"          ==   "CONST before"
    1.22 +  "_after"           ==   "CONST after"
    1.23    "_prime"           =>   "_after"
    1.24 -  "_unchanged"       ==   "unch"
    1.25 -  "_SqAct"           ==   "SqAct"
    1.26 -  "_AnAct"           ==   "AnAct"
    1.27 -  "_Enabled"         ==   "enabled"
    1.28 +  "_unchanged"       ==   "CONST unch"
    1.29 +  "_SqAct"           ==   "CONST SqAct"
    1.30 +  "_AnAct"           ==   "CONST AnAct"
    1.31 +  "_Enabled"         ==   "CONST enabled"
    1.32    "w |= [A]_v"       <=   "_SqAct A v w"
    1.33    "w |= <A>_v"       <=   "_AnAct A v w"
    1.34    "s |= Enabled A"   <=   "_Enabled A s"
     2.1 --- a/src/HOL/TLA/Init.thy	Thu Feb 11 13:54:53 2010 +0100
     2.2 +++ b/src/HOL/TLA/Init.thy	Thu Feb 11 21:31:50 2010 +0100
     2.3 @@ -1,11 +1,10 @@
     2.4 -(*
     2.5 -    File:        TLA/Init.thy
     2.6 -    ID:          $Id$
     2.7 -    Author:      Stephan Merz
     2.8 -    Copyright:   1998 University of Munich
     2.9 +(*  Title:      HOL/TLA/Init.thy
    2.10 +    Author:     Stephan Merz
    2.11 +    Copyright:  1998 University of Munich
    2.12  
    2.13 -Introduces type of temporal formulas. Defines interface between
    2.14 -temporal formulas and its "subformulas" (state predicates and actions).
    2.15 +Introduces type of temporal formulas.  Defines interface between
    2.16 +temporal formulas and its "subformulas" (state predicates and
    2.17 +actions).
    2.18  *)
    2.19  
    2.20  theory Init
    2.21 @@ -26,12 +25,12 @@
    2.22    st2         :: "behavior => state"
    2.23  
    2.24  syntax
    2.25 -  TEMP       :: "lift => 'a"                          ("(TEMP _)")
    2.26 +  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
    2.27    "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
    2.28  
    2.29  translations
    2.30    "TEMP F"   => "(F::behavior => _)"
    2.31 -  "_Init"    == "Initial"
    2.32 +  "_Init"    == "CONST Initial"
    2.33    "sigma |= Init F"  <= "_Init F sigma"
    2.34  
    2.35  defs
     3.1 --- a/src/HOL/TLA/Intensional.thy	Thu Feb 11 13:54:53 2010 +0100
     3.2 +++ b/src/HOL/TLA/Intensional.thy	Thu Feb 11 21:31:50 2010 +0100
     3.3 @@ -1,8 +1,6 @@
     3.4 -(*
     3.5 -    File:        TLA/Intensional.thy
     3.6 -    ID:          $Id$
     3.7 -    Author:      Stephan Merz
     3.8 -    Copyright:   1998 University of Munich
     3.9 +(*  Title:      HOL/TLA/Intensional.thy
    3.10 +    Author:     Stephan Merz
    3.11 +    Copyright:  1998 University of Munich
    3.12  *)
    3.13  
    3.14  header {* A framework for "intensional" (possible-world based) logics
    3.15 @@ -95,11 +93,11 @@
    3.16    "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
    3.17  
    3.18  translations
    3.19 -  "_const"        == "const"
    3.20 -  "_lift"         == "lift"
    3.21 -  "_lift2"        == "lift2"
    3.22 -  "_lift3"        == "lift3"
    3.23 -  "_Valid"        == "Valid"
    3.24 +  "_const"        == "CONST const"
    3.25 +  "_lift"         == "CONST lift"
    3.26 +  "_lift2"        == "CONST lift2"
    3.27 +  "_lift3"        == "CONST lift3"
    3.28 +  "_Valid"        == "CONST Valid"
    3.29    "_RAll x A"     == "Rall x. A"
    3.30    "_REx x  A"     == "Rex x. A"
    3.31    "_REx1 x  A"    == "Rex! x. A"
    3.32 @@ -112,11 +110,11 @@
    3.33  
    3.34    "_liftEqu"      == "_lift2 (op =)"
    3.35    "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
    3.36 -  "_liftNot"      == "_lift Not"
    3.37 +  "_liftNot"      == "_lift (CONST Not)"
    3.38    "_liftAnd"      == "_lift2 (op &)"
    3.39    "_liftOr"       == "_lift2 (op | )"
    3.40    "_liftImp"      == "_lift2 (op -->)"
    3.41 -  "_liftIf"       == "_lift3 If"
    3.42 +  "_liftIf"       == "_lift3 (CONST If)"
    3.43    "_liftPlus"     == "_lift2 (op +)"
    3.44    "_liftMinus"    == "_lift2 (op -)"
    3.45    "_liftTimes"    == "_lift2 (op *)"
    3.46 @@ -126,12 +124,12 @@
    3.47    "_liftLeq"      == "_lift2 (op <=)"
    3.48    "_liftMem"      == "_lift2 (op :)"
    3.49    "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
    3.50 -  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
    3.51 -  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
    3.52 +  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
    3.53 +  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
    3.54    "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
    3.55 -  "_liftPair"     == "_lift2 Pair"
    3.56 -  "_liftCons"     == "lift2 Cons"
    3.57 -  "_liftApp"      == "lift2 (op @)"
    3.58 +  "_liftPair"     == "_lift2 (CONST Pair)"
    3.59 +  "_liftCons"     == "CONST lift2 (CONST Cons)"
    3.60 +  "_liftApp"      == "CONST lift2 (op @)"
    3.61    "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
    3.62    "_liftList x"   == "_liftCons x (_const [])"
    3.63  
     4.1 --- a/src/HOL/TLA/ROOT.ML	Thu Feb 11 13:54:53 2010 +0100
     4.2 +++ b/src/HOL/TLA/ROOT.ML	Thu Feb 11 21:31:50 2010 +0100
     4.3 @@ -1,7 +1,3 @@
     4.4 -(*  Title:      HOL/TLA/ROOT.ML
     4.5 -
     4.6 -Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
     4.7 -*)
     4.8 +(* The Temporal Logic of Actions *)
     4.9  
    4.10  use_thys ["TLA"];
    4.11 -
     5.1 --- a/src/HOL/TLA/Stfun.thy	Thu Feb 11 13:54:53 2010 +0100
     5.2 +++ b/src/HOL/TLA/Stfun.thy	Thu Feb 11 21:31:50 2010 +0100
     5.3 @@ -1,8 +1,6 @@
     5.4 -(*
     5.5 -    File:        TLA/Stfun.thy
     5.6 -    ID:          $Id$
     5.7 -    Author:      Stephan Merz
     5.8 -    Copyright:   1998 University of Munich
     5.9 +(*  Title:      HOL/TLA/Stfun.thy
    5.10 +    Author:     Stephan Merz
    5.11 +    Copyright:  1998 University of Munich
    5.12  *)
    5.13  
    5.14  header {* States and state functions for TLA as an "intensional" logic *}
    5.15 @@ -42,7 +40,7 @@
    5.16  
    5.17  translations
    5.18    "PRED P"   =>  "(P::state => _)"
    5.19 -  "_stvars"  ==  "stvars"
    5.20 +  "_stvars"  ==  "CONST stvars"
    5.21  
    5.22  defs
    5.23    (* Base variables may be assigned arbitrary (type-correct) values.
     6.1 --- a/src/HOL/TLA/TLA.thy	Thu Feb 11 13:54:53 2010 +0100
     6.2 +++ b/src/HOL/TLA/TLA.thy	Thu Feb 11 21:31:50 2010 +0100
     6.3 @@ -1,8 +1,6 @@
     6.4 -(*
     6.5 -    File:        TLA/TLA.thy
     6.6 -    ID:          $Id$
     6.7 -    Author:      Stephan Merz
     6.8 -    Copyright:   1998 University of Munich
     6.9 +(*  Title:      HOL/TLA/TLA.thy
    6.10 +    Author:     Stephan Merz
    6.11 +    Copyright:  1998 University of Munich
    6.12  *)
    6.13  
    6.14  header {* The temporal level of TLA *}
    6.15 @@ -1168,4 +1166,3 @@
    6.16    done
    6.17  
    6.18  end
    6.19 -