diff -r 68d6c5b336c1 -r 20c9590bb5f5 src/HOL/MicroJava/J/Term.thy --- 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)