changeset 16417 | 9bc16273c2d4 |
parent 16184 | 80617b8d33c5 |
child 24147 | edc90be09ac1 |
1.1 --- a/src/HOL/UNITY/UNITY.thy Fri Jun 17 11:35:35 2005 +0200 1.2 +++ b/src/HOL/UNITY/UNITY.thy Fri Jun 17 16:12:49 2005 +0200 1.3 @@ -10,7 +10,7 @@ 1.4 1.5 header {*The Basic UNITY Theory*} 1.6 1.7 -theory UNITY = Main: 1.8 +theory UNITY imports Main begin 1.9 1.10 typedef (Program) 1.11 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,