src/HOL/UNITY/Project.thy
changeset 7689 affe0c2fdfbf
parent 7630 d0e4a6f1f05c
child 7826 c6a8b73b6c2a
     1.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 04 13:45:31 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 04 13:47:28 1999 +0200
     1.3 @@ -8,15 +8,4 @@
     1.4  Inheritance of GUARANTEES properties under extension
     1.5  *)
     1.6  
     1.7 -Project = Extend +
     1.8 -
     1.9 -
    1.10 -constdefs
    1.11 -
    1.12 -  restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
    1.13 -    "restr_act C h act == project_act C h (extend_act h act)"
    1.14 -
    1.15 -  restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
    1.16 -    "restr C h F == project C h (extend h F)"
    1.17 -
    1.18 -end
    1.19 +Project = Extend