--- a/src/HOL/UNITY/Extend.thy Tue Sep 21 10:39:33 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Tue Sep 21 11:09:24 1999 +0200
@@ -25,10 +25,10 @@
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
"extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
+ (*Argument C allows weak safety laws to be projected*)
project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
"project_act C h act ==
- {(x,x'). EX y y'. (h(x,y), h(x',y')) : act &
- (x = x' | h(x,y) : C)}"
+ {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),