Basis now Main.
authornipkow
Wed, 24 Nov 1999 12:12:36 +0100
changeset 8029 05446a898852
parent 8028 5357e8eb09c8
child 8030 af8db1872960
Basis now Main.
src/HOL/IMP/Com.thy
src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Com.thy	Wed Nov 24 10:25:28 1999 +0100
+++ b/src/HOL/IMP/Com.thy	Wed Nov 24 12:12:36 1999 +0100
@@ -7,7 +7,7 @@
 Syntax of commands
 *)
 
-Com = Datatype +
+Com = Main +
 
 types 
       val
--- a/src/HOL/IMP/Transition.thy	Wed Nov 24 10:25:28 1999 +0100
+++ b/src/HOL/IMP/Transition.thy	Wed Nov 24 12:12:36 1999 +0100
@@ -6,7 +6,7 @@
 Transition semantics of commands
 *)
 
-Transition = Natural + RelPow +
+Transition = Natural +
 
 consts  evalc1    :: "((com*state)*(com*state))set"