--- a/src/HOL/UNITY/Lift_prog.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Mon Oct 18 15:18:24 1999 +0200
@@ -22,19 +22,19 @@
lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
"lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
- (*Argument C allows weak safety laws to be projected*)
- drop_act :: "[('a=>'b) set, 'a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
- "drop_act C i act == {(f i, f' i) | f f'. (f,f'): act & f: C}"
+ drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
+ "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
lift_prog :: "['a, 'b program] => ('a => 'b) program"
"lift_prog i F ==
mk_program (lift_set i (Init F),
lift_act i `` Acts F)"
+ (*Argument C allows weak safety laws to be projected*)
drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
"drop_prog C i F ==
mk_program (drop_set i (Init F),
- drop_act C i `` (Acts F))"
+ drop_act i `` Restrict C `` (Acts F))"
(*simplifies the expression of specifications*)
constdefs