--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Feb 11 00:45:02 2010 +0100
@@ -584,10 +584,9 @@
(* Currently: empty exception_table *)
-syntax
+abbreviation (input)
empty_et :: exception_table
-translations
- "empty_et" => "[]"
+ where "empty_et == []"
@@ -860,12 +859,13 @@
section "Correspondence bytecode - method types"
(* ********************************************************************** *)
-syntax
+abbreviation (input)
ST_of :: "state_type \<Rightarrow> opstack_type"
+ where "ST_of == fst"
+
+abbreviation (input)
LT_of :: "state_type \<Rightarrow> locvars_type"
-translations
- "ST_of" => "fst"
- "LT_of" => "snd"
+ where "LT_of == snd"
lemma states_lower:
"\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk>