src/HOL/UNITY/Project.thy
changeset 7947 b999c1ab9327
parent 7880 62fb24e28e5e
child 8055 bb15396278fb
     1.1 --- a/src/HOL/UNITY/Project.thy	Wed Oct 27 13:02:23 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Project.thy	Wed Oct 27 13:03:32 1999 +0200
     1.3 @@ -19,8 +19,7 @@
     1.4    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
     1.5  		 'c program set, 'c program set, 'a program set] => bool"
     1.6    "extending C h F X' Y' Y ==
     1.7 -     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
     1.8 -            Disjoint UNIV (extend h F) G
     1.9 +     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
    1.10              --> extend h F Join G : Y'"
    1.11  
    1.12  end