src/HOL/UNITY/Project.thy
changeset 7689 affe0c2fdfbf
parent 7630 d0e4a6f1f05c
child 7826 c6a8b73b6c2a
--- a/src/HOL/UNITY/Project.thy	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Mon Oct 04 13:47:28 1999 +0200
@@ -8,15 +8,4 @@
 Inheritance of GUARANTEES properties under extension
 *)
 
-Project = Extend +
-
-
-constdefs
-
-  restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
-    "restr_act C h act == project_act C h (extend_act h act)"
-
-  restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
-    "restr C h F == project C h (extend h F)"
-
-end
+Project = Extend