src/HOL/UNITY/Extend.thy
changeset 10834 a7897aebbffc
parent 10064 1a77667b21ef
child 13790 8d7e9fce8c50
     1.1 --- a/src/HOL/UNITY/Extend.thy	Tue Jan 09 15:29:17 2001 +0100
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Tue Jan 09 15:32:27 2001 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4       (*Using the locale constant "f", this is  f (h (x,y))) = x*)
     1.5    
     1.6    extend_set :: "['a*'b => 'c, 'a set] => 'c set"
     1.7 -    "extend_set h A == h `` (A <*> UNIV)"
     1.8 +    "extend_set h A == h ` (A <*> UNIV)"
     1.9  
    1.10    project_set :: "['a*'b => 'c, 'c set] => 'a set"
    1.11      "project_set h C == {x. EX y. h(x,y) : C}"
    1.12 @@ -34,16 +34,16 @@
    1.13  
    1.14    extend :: "['a*'b => 'c, 'a program] => 'c program"
    1.15      "extend h F == mk_program (extend_set h (Init F),
    1.16 -			       extend_act h `` Acts F,
    1.17 -			       project_act h -`` AllowedActs F)"
    1.18 +			       extend_act h ` Acts F,
    1.19 +			       project_act h -` AllowedActs F)"
    1.20  
    1.21    (*Argument C allows weak safety laws to be projected*)
    1.22    project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
    1.23      "project h C F ==
    1.24         mk_program (project_set h (Init F),
    1.25 -		   project_act h `` Restrict C `` Acts F,
    1.26 +		   project_act h ` Restrict C ` Acts F,
    1.27  		   {act. Restrict (project_set h C) act :
    1.28 -		         project_act h `` Restrict C `` AllowedActs F})"
    1.29 +		         project_act h ` Restrict C ` AllowedActs F})"
    1.30  
    1.31  locale Extend =
    1.32    fixes