src/HOL/TLA/Action.thy
changeset 47968 3119ad2b5ad3
parent 42814 5af15f1e2ef6
child 52037 837211662fb8
     1.1 --- a/src/HOL/TLA/Action.thy	Wed May 23 16:22:27 2012 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed May 23 16:53:12 2012 +0200
     1.3 @@ -58,11 +58,13 @@
     1.4    "s |= Enabled A"   <=   "_Enabled A s"
     1.5    "w |= unchanged f" <=   "_unchanged f w"
     1.6  
     1.7 -axioms
     1.8 -  unl_before:    "(ACT $v) (s,t) == v s"
     1.9 -  unl_after:     "(ACT v$) (s,t) == v t"
    1.10 +axiomatization where
    1.11 +  unl_before:    "(ACT $v) (s,t) == v s" and
    1.12 +  unl_after:     "(ACT v$) (s,t) == v t" and
    1.13  
    1.14    unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
    1.15 +
    1.16 +defs
    1.17    square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    1.18    angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.19