src/HOL/TLA/Action.thy
changeset 35108 e384e27c229f
parent 30528 7173bf123335
child 35318 e1b61c5fd494
     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"