src/HOL/MicroJava/J/Term.thy
changeset 10119 20c9590bb5f5
parent 10069 c7226e6f9625
child 10763 08e1610c1dcb
--- a/src/HOL/MicroJava/J/Term.thy	Sat Sep 30 12:27:57 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Mon Oct 02 12:35:48 2000 +0200
@@ -6,7 +6,7 @@
 Java expressions and statements
 *)
 
-Term = Value + 
+Term = Value +
 
 datatype binop = Eq | Add    (* function codes for binary operation *)
 
@@ -23,7 +23,7 @@
   | Call expr mname 
     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
 
-and stmt
+datatype stmt
   = Skip                     (* empty statement *)
   | Expr expr                (* expression statement *)
   | Comp stmt stmt       ("_;; _"             [61,60]60)