src/HOL/UNITY/Comp/Counterc.thy
changeset 13812 91713a1915ee
parent 13792 d1811693899c
child 14088 61bd46feb919
     1.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4   "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
     1.5   
     1.6    Component :: "nat => state program"
     1.7 -  "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
     1.8 -	       UN G: preserves (%s. (c s) i). Acts G)"
     1.9 +  "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
    1.10 +				   {a i},
    1.11 + 	                           \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
    1.12  end