--- a/src/HOL/NanoJava/Term.thy Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/Term.thy Sun Aug 21 22:13:04 2011 +0200
@@ -11,14 +11,13 @@
typedecl fname --{* field name *}
typedecl vname --{* variable name *}
-consts
- This :: vname --{* This pointer *}
- Par :: vname --{* method parameter *}
+axiomatization
+ This --{* This pointer *}
+ Par --{* method parameter *}
Res :: vname --{* method result *}
-
-text {* Inequality axioms are not required for the meta theory. *}
+ -- {* Inequality axioms are not required for the meta theory. *}
(*
-axioms
+where
This_neq_Par [simp]: "This \<noteq> Par"
Par_neq_Res [simp]: "Par \<noteq> Res"
Res_neq_This [simp]: "Res \<noteq> This"