--- a/src/HOL/UNITY/Extend.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy Sat Sep 23 16:02:01 2000 +0200
@@ -34,12 +34,16 @@
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
- extend_act h `` Acts F)"
+ extend_act h `` Acts F,
+ project_act h -`` AllowedActs F)"
(*Argument C allows weak safety laws to be projected*)
project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
- "project h C F == mk_program (project_set h (Init F),
- project_act h `` Restrict C `` Acts F)"
+ "project h C F ==
+ mk_program (project_set h (Init F),
+ project_act h `` Restrict C `` Acts F,
+ {act. Restrict (project_set h C) act :
+ project_act h `` Restrict C `` AllowedActs F})"
locale Extend =
fixes