# HG changeset patch
# User nipkow
# Date 970482948 -7200
# Node ID 20c9590bb5f5186bbc1ce4b445748ace5d38b04b
# Parent  68d6c5b336c19d05e560839e1d1debda78fbc529
separated expr and stmt

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)