# HG changeset patch
# User nipkow
# Date 943441956 -3600
# Node ID 05446a898852ea5eef87468fb67e8dd7ec3896d0
# Parent  5357e8eb09c8d83618ba1003f507dcdc3cbe21bc
Basis now Main.

diff -r 5357e8eb09c8 -r 05446a898852 src/HOL/IMP/Com.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
diff -r 5357e8eb09c8 -r 05446a898852 src/HOL/IMP/Transition.thy
--- 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"