Basis now Main.
authornipkow
Wed, 24 Nov 1999 12:12:36 +0100
changeset 802905446a898852
parent 8028 5357e8eb09c8
child 8030 af8db1872960
Basis now Main.
src/HOL/IMP/Com.thy
src/HOL/IMP/Transition.thy
     1.1 --- a/src/HOL/IMP/Com.thy	Wed Nov 24 10:25:28 1999 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Nov 24 12:12:36 1999 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  Syntax of commands
     1.5  *)
     1.6  
     1.7 -Com = Datatype +
     1.8 +Com = Main +
     1.9  
    1.10  types 
    1.11        val
     2.1 --- a/src/HOL/IMP/Transition.thy	Wed Nov 24 10:25:28 1999 +0100
     2.2 +++ b/src/HOL/IMP/Transition.thy	Wed Nov 24 12:12:36 1999 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  Transition semantics of commands
     2.5  *)
     2.6  
     2.7 -Transition = Natural + RelPow +
     2.8 +Transition = Natural +
     2.9  
    2.10  consts  evalc1    :: "((com*state)*(com*state))set"
    2.11