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