src/HOL/UNITY/Project.thy
changeset 7880 62fb24e28e5e
parent 7878 43b03d412b82
child 7947 b999c1ab9327
     1.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 18 15:20:21 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 18 16:16:03 1999 +0200
     1.3 @@ -14,12 +14,12 @@
     1.4    projecting :: "['c program => 'c set, 'a*'b => 'c, 
     1.5  		  'a program, 'c program set, 'a program set] => bool"
     1.6    "projecting C h F X' X ==
     1.7 -     ALL G. extend h F Join G : X' --> F Join project (C G) h G : X"
     1.8 +     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
     1.9  
    1.10    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    1.11  		 'c program set, 'c program set, 'a program set] => bool"
    1.12    "extending C h F X' Y' Y ==
    1.13 -     ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
    1.14 +     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
    1.15              Disjoint UNIV (extend h F) G
    1.16              --> extend h F Join G : Y'"
    1.17