src/HOL/TLA/Init.thy
changeset 35108 e384e27c229f
parent 26304 02fbd0e7954a
child 35318 e1b61c5fd494
     1.1 --- a/src/HOL/TLA/Init.thy	Thu Feb 11 13:54:53 2010 +0100
     1.2 +++ b/src/HOL/TLA/Init.thy	Thu Feb 11 21:31:50 2010 +0100
     1.3 @@ -1,11 +1,10 @@
     1.4 -(*
     1.5 -    File:        TLA/Init.thy
     1.6 -    ID:          $Id$
     1.7 -    Author:      Stephan Merz
     1.8 -    Copyright:   1998 University of Munich
     1.9 +(*  Title:      HOL/TLA/Init.thy
    1.10 +    Author:     Stephan Merz
    1.11 +    Copyright:  1998 University of Munich
    1.12  
    1.13 -Introduces type of temporal formulas. Defines interface between
    1.14 -temporal formulas and its "subformulas" (state predicates and actions).
    1.15 +Introduces type of temporal formulas.  Defines interface between
    1.16 +temporal formulas and its "subformulas" (state predicates and
    1.17 +actions).
    1.18  *)
    1.19  
    1.20  theory Init
    1.21 @@ -26,12 +25,12 @@
    1.22    st2         :: "behavior => state"
    1.23  
    1.24  syntax
    1.25 -  TEMP       :: "lift => 'a"                          ("(TEMP _)")
    1.26 +  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
    1.27    "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
    1.28  
    1.29  translations
    1.30    "TEMP F"   => "(F::behavior => _)"
    1.31 -  "_Init"    == "Initial"
    1.32 +  "_Init"    == "CONST Initial"
    1.33    "sigma |= Init F"  <= "_Init F sigma"
    1.34  
    1.35  defs