--- a/src/HOL/NanoJava/Term.thy Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Fri Sep 21 18:23:15 2001 +0200
@@ -18,7 +18,7 @@
Par :: vname --{* method parameter *}
Res :: vname --{* method result *}
-text {* Inequality axioms not required here *}
+text {* Inequality axioms are not required for the meta theory. *}
(*
axioms
This_neq_Par [simp]: "This \<noteq> Par"
@@ -29,8 +29,8 @@
datatype stmt
= Skip --{* empty statement *}
| Comp stmt stmt ("_;; _" [91,90 ] 90)
- | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
- | Loop vname stmt ("While '(_') _" [99,91 ] 91)
+ | Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91)
+ | Loop vname stmt ("While '(_') _" [ 3,91 ] 91)
| LAss vname expr ("_ :== _" [99, 95] 94) --{* local assignment *}
| FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field assignment *}
| Meth "cname \<times> mname" --{* virtual method *}