src/HOL/IMP/Com.thy
changeset 12338 de0f4a63baa5
parent 9241 f961c1fdff50
child 12431 07ec657249e5
     1.1 --- a/src/HOL/IMP/Com.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4        aexp  = state => val
     1.5        bexp  = state => bool
     1.6  
     1.7 -arities loc :: term
     1.8 +arities loc :: type
     1.9  
    1.10  datatype
    1.11    com = SKIP