src/HOL/UNITY/Extend.thy
changeset 7546 36b26759147e
parent 7537 875754b599df
child 7826 c6a8b73b6c2a
     1.1 --- a/src/HOL/UNITY/Extend.thy	Tue Sep 21 10:39:33 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Tue Sep 21 11:09:24 1999 +0200
     1.3 @@ -25,10 +25,10 @@
     1.4    extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     1.5      "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
     1.6  
     1.7 +  (*Argument C allows weak safety laws to be projected*)
     1.8    project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
     1.9      "project_act C h act ==
    1.10 -         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act &
    1.11 -	                   (x = x' | h(x,y) : C)}"
    1.12 +         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
    1.13  
    1.14    extend :: "['a*'b => 'c, 'a program] => 'c program"
    1.15      "extend h F == mk_program (extend_set h (Init F),