# HG changeset patch
# User wenzelm
# Date 1265759116 -3600
# Node ID af4c18c30593626654dcdd21b27581d71fc05e1c
# Parent  894e82be8d05ccb8b7390dfa0e967655c1610b7b
modernized syntax translations, using mostly abbreviation/notation;
minor tuning;

diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/AxExample.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -166,7 +166,7 @@
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
      (* just for clarification: *)
-apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
+apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2)
 prefer 2
 apply   (simp add: invocation_declclass_def dynmethd_def)
 apply   (unfold dynlookup_def)
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/AxSem.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -6,7 +6,6 @@
 header {* Axiomatic semantics of Java expressions and statements 
           (see also Eval.thy)
         *}
-
 theory AxSem imports Evaln TypeSafe begin
 
 text {*
@@ -39,14 +38,15 @@
 *}
 
 types  res = vals --{* result entry *}
-syntax
-  Val  :: "val      \<Rightarrow> res"
-  Var  :: "var      \<Rightarrow> res"
-  Vals :: "val list \<Rightarrow> res"
-translations
-  "Val  x"     => "(In1 x)"
-  "Var  x"     => "(In2 x)"
-  "Vals x"     => "(In3 x)"
+
+abbreviation (input)
+  Val where "Val x == In1 x"
+
+abbreviation (input)
+  Var where "Var x == In2 x"
+
+abbreviation (input)
+  Vals where "Vals x == In3 x"
 
 syntax
   "_Val"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
@@ -54,9 +54,9 @@
   "_Vals"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
 
 translations
-  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
-  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> the_In2"
-  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> the_In3"
+  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> CONST the_In1"
+  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> CONST the_In2"
+  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
 
   --{* relation on result values, state and auxiliary variables *}
 types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -105,10 +105,9 @@
 apply auto
 done
 
-syntax
-  Normal     :: "'a assn \<Rightarrow> 'a assn"
-translations
-  "Normal P" == "P \<and>. normal"
+abbreviation
+  Normal :: "'a assn \<Rightarrow> 'a assn"
+  where "Normal P == P \<and>. normal"
 
 lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
 apply (rule ext)
@@ -207,9 +206,9 @@
  "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
 
 syntax
-"@peek_res"  :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
+  "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
 translations
-  "\<lambda>w:. P"   == "peek_res (\<lambda>w. P)"
+  "\<lambda>w:. P"   == "CONST peek_res (\<lambda>w. P)"
 
 lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
 apply (unfold peek_res_def)
@@ -268,9 +267,9 @@
  "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
 
 syntax
-"@peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
+  "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
 translations
-  "\<lambda>s.. P"   == "peek_st (\<lambda>s. P)"
+  "\<lambda>s.. P"   == "CONST peek_st (\<lambda>s. P)"
 
 lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
 apply (unfold peek_st_def)
@@ -386,33 +385,31 @@
                                         ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
 types    'a triples = "'a triple set"
 
-syntax
-
+abbreviation
   var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
                                          ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75)
+  where "{P} e=> {Q} == {P} In2  e> {Q}"
+
+abbreviation
   expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
                                          ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75)
+  where "{P} e-> {Q} == {P} In1l e> {Q}"
+
+abbreviation
   exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
                                          ("{(1_)}/ _#>/ {(1_)}"    [3,65,3] 75)
+  where "{P} e#> {Q} == {P} In3  e> {Q}"
+
+abbreviation
   stmt_triple  :: "['a assn, stmt,        'a assn] \<Rightarrow> 'a triple"
                                          ("{(1_)}/ ._./ {(1_)}"     [3,65,3] 75)
-
-syntax (xsymbols)
+  where "{P} .c. {Q} == {P} In1r c> {Q}"
 
-  triple       :: "['a assn, term        ,'a assn] \<Rightarrow> 'a triple"
-                                         ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
-  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
-                                         ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
-  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
-                                         ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
-  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
-                                         ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
-
-translations
-  "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
-  "{P} e=\<succ> {Q}" == "{P} In2  e\<succ> {Q}"
-  "{P} e\<doteq>\<succ> {Q}" == "{P} In3  e\<succ> {Q}"
-  "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
+notation (xsymbols)
+  triple  ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75) and
+  var_triple  ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75) and
+  expr_triple  ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75) and
+  exprs_triple  ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
 
 lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
 apply (rule inj_onI)
@@ -436,26 +433,25 @@
     ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
                                                 ("_,_|\<Turnstile>_"   [61,58,58] 57)
 
-syntax
-
+abbreviation
  triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
                                                 (  "_||=_:_" [61,0, 58] 57)
-     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
-                                                ( "_,_|=_"   [61,58,58] 57)
-
-syntax (xsymbols)
+ where "G||=n:ts == Ball ts (triple_valid G n)"
 
- triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
-                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
-     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
-                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
+abbreviation
+ ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
+                                                ( "_,_|=_"   [61,58,58] 57)
+ where "G,A |=t == G,A|\<Turnstile>{t}"
+
+notation (xsymbols)
+  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
+  ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
 
 defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
                           \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
                           (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
-translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
-defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
-translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
+
+defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
 
 lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
  (\<forall>Y s Z. P Y s Z 
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Basis.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -27,12 +27,8 @@
 apply fast+
 done
 
-syntax
-  "3" :: nat   ("3") 
-  "4" :: nat   ("4")
-translations
- "3" == "Suc 2"
- "4" == "Suc 3"
+abbreviation nat3 :: nat  ("3") where "3 == Suc 2"
+abbreviation nat4 :: nat  ("4") where "4 == Suc 3"
 
 (*unused*)
 lemma range_bool_domain: "range f = {f True, f False}"
@@ -182,10 +178,7 @@
 
 hide const In0 In1
 
-syntax
-  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
-translations
- "fun_sum" == "CONST sum_case"
+notation sum_case  (infixr "'(+')"80)
 
 consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
           the_Inr  :: "'a + 'b \<Rightarrow> 'b"
@@ -201,18 +194,17 @@
 primrec  "the_In2 (In2 b) = b"
 primrec  "the_In3 (In3 c) = c"
 
-syntax
-         In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-         In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-translations
-        "In1l e" == "In1 (CONST Inl e)"
-        "In1r c" == "In1 (CONST Inr c)"
+abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
+      where "In1l e == In1 (Inl e)"
+
+abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
+      where "In1r c == In1 (Inr c)"
 
-syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
-       the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
-translations
-   "the_In1l" == "the_Inl \<circ> the_In1"
-   "the_In1r" == "the_Inr \<circ> the_In1"
+abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
+      where "the_In1l == the_Inl \<circ> the_In1"
+
+abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
+      where "the_In1r == the_Inr \<circ> the_In1"
 
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
@@ -319,8 +311,8 @@
 syntax
   "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
 translations
-  "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
-  "%x#xs  . b"  == "lsplit (%x xs  . b)"
+  "%y#x#xs. b"  == "CONST lsplit (%y x#xs. b)"
+  "%x#xs  . b"  == "CONST lsplit (%x xs  . b)"
 
 lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
 apply (unfold lsplit_def)
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Decl.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -402,17 +402,21 @@
      "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
      "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
 
-syntax
-  iface     :: "prog  \<Rightarrow> (qtname, iface) table"
-  "class"     :: "prog  \<Rightarrow> (qtname, class) table"
-  is_iface  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
-  is_class  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
+abbreviation
+  iface :: "prog  \<Rightarrow> (qtname, iface) table"
+  where "iface G I == table_of (ifaces G) I"
+
+abbreviation
+  "class" :: "prog  \<Rightarrow> (qtname, class) table"
+  where "class G C == table_of (classes G) C"
 
-translations
-           "iface G I" == "table_of (ifaces G) I"
-           "class G C" == "table_of (classes G) C"
-        "is_iface G I" == "iface G I \<noteq> None"
-        "is_class G C" == "class G C \<noteq> None"
+abbreviation
+  is_iface :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
+  where "is_iface G I == iface G I \<noteq> None"
+
+abbreviation
+  is_class :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
+  where "is_class G C == class G C \<noteq> None"
 
 
 section "is type"
@@ -445,21 +449,22 @@
   subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
   subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
 
-syntax
- "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+abbreviation
+  subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+  where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
+
+abbreviation
+  subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+  where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
 
-syntax (xsymbols)
-  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
-  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
-  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
+abbreviation
+  subcls_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+  where "G|-C <:C D == (C,D) \<in>(subcls1 G)^+"
 
-translations
-        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
-        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
-        "G\<turnstile>C \<prec>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^+"
- 
+notation (xsymbols)
+  subcls1_syntax  ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70) and
+  subclseq_syntax  ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70) and
+  subcls_syntax  ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
 
 lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
                  \<Longrightarrow> (I,J) \<in> subint1 G" 
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -13,8 +13,8 @@
 "is_public G qn \<equiv> (case class G qn of
                      None       \<Rightarrow> (case iface G qn of
                                       None       \<Rightarrow> False
-                                    | Some iface \<Rightarrow> access iface = Public)
-                   | Some class \<Rightarrow> access class = Public)"
+                                    | Some i \<Rightarrow> access i = Public)
+                   | Some c \<Rightarrow> access c = Public)"
 
 subsection "accessibility of types (cf. 6.6.1)"
 text {* 
@@ -445,21 +445,17 @@
      | Protected \<Rightarrow> True
      | Public    \<Rightarrow> True)"
 
-syntax
-Method_inheritable_in::
+abbreviation
+Method_inheritable_in_syntax::
  "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
                 ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
+ where "G\<turnstile>Method m inheritable_in p == G\<turnstile>methdMembr m inheritable_in p"
 
-translations
-"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
-
-syntax
+abbreviation
 Methd_inheritable_in::
  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
                 ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
-
-translations
-"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
+ where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p"
 
 subsubsection "declared-in/undeclared-in"
 
@@ -486,17 +482,15 @@
                         fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
                       | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
 
-syntax
+abbreviation
 method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
                                  ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
-translations
-"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
+ where "G\<turnstile>Method m declared_in C == G\<turnstile>mdecl (mthd m) declared_in C"
 
-syntax
+abbreviation
 methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
                                ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
-translations
-"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
+ where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C"
 
 lemma declared_in_classD:
  "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
@@ -538,26 +532,20 @@
 of S will not inherit the member, regardless if they are in the same
 package as A or not.*}
 
-syntax
+abbreviation
 method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
                            ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
+ where "G\<turnstile>Method m member_of C == G\<turnstile>(methdMembr m) member_of C"
 
-translations
- "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
-
-syntax
+abbreviation
 methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
                            ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
+ where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C" 
 
-translations
- "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
-
-syntax
+abbreviation
 fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
                            ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
-
-translations
- "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
+ where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
 
 constdefs
 inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
@@ -578,19 +566,15 @@
 is necessary since not all members are inherited to subclasses. So such
 members are not member-of the subclass but member-in the subclass.*}
 
-syntax
+abbreviation
 method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
                            ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
+ where "G\<turnstile>Method m member_in C == G\<turnstile>(methdMembr m) member_in C"
 
-translations
- "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
-
-syntax
+abbreviation
 methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
                            ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
-
-translations
- "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
+ where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C"
 
 lemma member_inD: "G\<turnstile>m member_in C 
  \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
@@ -649,18 +633,16 @@
 | Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
             \<Longrightarrow> G\<turnstile>new overrides old"
 
-syntax
+abbreviation (input)
 sig_stat_overrides:: 
  "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
                                   ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
+ where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
 
-syntax
+abbreviation (input)
 sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
                                   ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
+ where "G,s\<turnstile>new overrides old == G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"
 
 subsubsection "Hiding"
 
@@ -674,11 +656,10 @@
     G\<turnstile>Method old declared_in (declclass old) \<and> 
     G\<turnstile>Method old inheritable_in pid (declclass new)"
 
-syntax
-sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
+abbreviation
+sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
                                   ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
-translations
- "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
+ where "G,s\<turnstile>new hides old == G\<turnstile>(qmdecl s new) hides (qmdecl s old)"
 
 lemma hidesI:
 "\<lbrakk>is_static new; msig new = msig old;
@@ -731,14 +712,14 @@
  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
                    ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
 
-"G\<turnstile>membr in class permits_acc_from accclass 
+"G\<turnstile>membr in cls permits_acc_from accclass 
   \<equiv> (case (accmodi membr) of
        Private   \<Rightarrow> (declclass membr = accclass)
      | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
      | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
                     \<or>
                     (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
-                     \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
+                     \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
      | Public    \<Rightarrow> True)"
 text {*
 The subcondition of the @{term "Protected"} case: 
@@ -774,12 +755,14 @@
 
 | "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
 
-| Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
+| Immediate:  "!!membr class.
+               \<lbrakk>G\<turnstile>membr member_of class;
                 G\<turnstile>(Class class) accessible_in (pid accclass);
                 G\<turnstile>membr in class permits_acc_from accclass 
                \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
 
-| Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
+| Overriding: "!!membr class C new old supr.
+               \<lbrakk>G\<turnstile>membr member_of class;
                 G\<turnstile>(Class class) accessible_in (pid accclass);
                 membr=(C,mdecl new);
                 G\<turnstile>(C,new) overrides\<^sub>S old; 
@@ -787,23 +770,21 @@
                 G\<turnstile>Method old of supr accessible_from accclass
                \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
 
-syntax 
+abbreviation
 methd_accessible_from:: 
  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
                  ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
+ where
+ "G\<turnstile>Methd s m of cls accessible_from accclass ==
+   G\<turnstile>(method s m) of cls accessible_from accclass"
 
-translations
-"G\<turnstile>Methd s m of cls accessible_from accclass"  
- \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
-
-syntax 
+abbreviation
 field_accessible_from:: 
  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
                  ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
-
-translations
-"G\<turnstile>Field fn f of C accessible_from accclass"  
- \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
+ where
+ "G\<turnstile>Field fn f of C accessible_from accclass ==
+  G\<turnstile>(fieldm fn f) of C accessible_from accclass"
 
 inductive
   dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -817,34 +798,32 @@
 
 | "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
 
-| Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
+| Immediate:  "!!class. \<lbrakk>G\<turnstile>membr member_in class;
                 G\<turnstile>membr in class permits_acc_from accclass 
                \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
 
-| Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
+| Overriding: "!!class. \<lbrakk>G\<turnstile>membr member_in class;
                 membr=(C,mdecl new);
                 G\<turnstile>(C,new) overrides old; 
                 G\<turnstile>class \<prec>\<^sub>C supr;
                 G\<turnstile>Method old in supr dyn_accessible_from accclass
                \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
 
-syntax 
+abbreviation
 methd_dyn_accessible_from:: 
  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
              ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
+ where
+ "G\<turnstile>Methd s m in C dyn_accessible_from accC ==
+  G\<turnstile>(method s m) in C dyn_accessible_from accC"  
 
-translations
-"G\<turnstile>Methd s m in C dyn_accessible_from accC"  
- \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
-
-syntax 
+abbreviation
 field_dyn_accessible_from:: 
  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
          ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
-
-translations
-"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
- \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
+ where
+ "G\<turnstile>Field fn f in dynC dyn_accessible_from accC ==
+  G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
 
 
 lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Eval.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -125,20 +125,21 @@
  assignment. 
 *}
 
-syntax (xsymbols)
+abbreviation (xsymbols)
   dummy_res :: "vals" ("\<diamondsuit>")
-translations
-  "\<diamondsuit>" == "In1 Unit"
+  where "\<diamondsuit> == In1 Unit"
+
+abbreviation (input)
+  val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
+  where "\<lfloor>e\<rfloor>\<^sub>e == In1 e"
 
-syntax 
-  val_inj_vals:: "expr \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
-  var_inj_vals::  "var \<Rightarrow> term"  ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
-  lst_inj_vals:: "expr list \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+abbreviation (input)
+  var_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
+  where "\<lfloor>v\<rfloor>\<^sub>v == In2 v"
 
-translations 
-  "\<lfloor>e\<rfloor>\<^sub>e" \<rightharpoonup> "In1 e"
-  "\<lfloor>v\<rfloor>\<^sub>v" \<rightharpoonup> "In2 v"
-  "\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+  lst_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+  where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
 
 constdefs
   undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Example.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -1202,74 +1202,52 @@
 
 abbreviation "one == Suc 0"
 abbreviation "two == Suc one"
-abbreviation "tree == Suc two"
-abbreviation "four == Suc tree"
+abbreviation "three == Suc two"
+abbreviation "four == Suc three"
+
+abbreviation
+  "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
+                ,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
 
-syntax
-  obj_a :: obj
-  obj_b :: obj
-  obj_c :: obj
-  arr_N :: "(vn, val) table"
-  arr_a :: "(vn, val) table"
-  globs1 :: globs
-  globs2 :: globs
-  globs3 :: globs
-  globs8 :: globs
-  locs3 :: locals
-  locs4 :: locals
-  locs8 :: locals
-  s0  :: state
-  s0' :: state
-  s9' :: state
-  s1  :: state
-  s1' :: state
-  s2  :: state
-  s2' :: state
-  s3  :: state
-  s3' :: state
-  s4  :: state
-  s4' :: state
-  s6' :: state
-  s7' :: state
-  s8  :: state
-  s8' :: state
+abbreviation
+  "obj_b == \<lparr>tag=CInst Ext
+                ,values=(empty(Inl (vee, Base)\<mapsto>Null   )
+                              (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
+
+abbreviation
+  "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
+
+abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
+abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
+
+abbreviation
+  "globs1 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
+                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)"
 
-translations
-  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
-                ,values=CONST empty(CONST Inr 0\<mapsto>Bool False)(CONST Inr (CONST one)\<mapsto>Bool False)\<rparr>"
-  "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
-                ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
-                              (CONST Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
-  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
-  "arr_N"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Null)"
-  "arr_a"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
-  "globs1"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
-                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
-                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
-  "globs2"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
-                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
-                     (CONST Inl a\<mapsto>obj_a)
-                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
-  "globs3"  == "globs2(CONST Inl b\<mapsto>obj_b)"
-  "globs8"  == "globs3(CONST Inl c\<mapsto>obj_c)"
-  "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
-  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(CONST Inr()\<mapsto>Addr b)"
-  "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
-  "s0"  == "       st (CONST empty) (CONST empty)"
-  "s0'" == " Norm  s0"
-  "s1"  == "       st globs1 (CONST empty)"
-  "s1'" == " Norm  s1"
-  "s2"  == "       st globs2 (CONST empty)"
-  "s2'" == " Norm  s2"
-  "s3"  == "       st globs3 locs3 "
-  "s3'" == " Norm  s3"
-  "s4"  == "       st globs3 locs4"
-  "s4'" == " Norm  s4"
-  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
-  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
-  "s8"  == "       st globs8 locs8"
-  "s8'" == " Norm  s8"
-  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
+abbreviation
+  "globs2 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
+                     (Inl a\<mapsto>obj_a)
+                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
+
+abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
+abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
+abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
+abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
+
+abbreviation "s0 == st empty empty"
+abbreviation "s0' == Norm  s0"
+abbreviation "s1 == st globs1 empty"
+abbreviation "s1' == Norm s1"
+abbreviation "s2 == st globs2 empty"
+abbreviation "s2' == Norm s2"
+abbreviation "s3 == st globs3 locs3"
+abbreviation "s3' == Norm s3"
+abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)"
+abbreviation "s8 == st globs8 locs8"
+abbreviation "s8' == Norm s8"
+abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
 
 
 declare Pair_eq [simp del]
@@ -1293,7 +1271,7 @@
 apply  (rule eval_Is (* NewC *))
       (* begin init Ext *)
 apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
-apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
+apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
 apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
 apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
 apply   (rule eval_Is (* Init Ext *))
@@ -1336,7 +1314,7 @@
 apply (drule alloc_one)
 apply  (simp (no_asm_simp))
 apply clarsimp
-apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
+apply (erule_tac V = "atleast_free ?h three" in thin_rl)
 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
 apply (simp (no_asm_use))
 apply (rule eval_Is (* Try *))
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Name.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -20,13 +20,11 @@
 datatype lname        --{* names for local variables and the This pointer *}
         = EName ename 
         | This
-syntax   
-  VName  :: "vname \<Rightarrow> lname"
-  Result :: lname
+abbreviation VName   :: "vname \<Rightarrow> lname"
+      where "VName n == EName (VNam n)"
 
-translations
-  "VName n" == "EName (VNam n)"
-  "Result"  == "EName Res"
+abbreviation Result :: lname
+      where "Result == EName Res"
 
 datatype xname          --{* names of standard exceptions *}
         = Throwable
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/State.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -254,13 +254,11 @@
 by (simp add: heap_def)
 
 
-syntax
-  val_this     :: "st \<Rightarrow> val"
-  lookup_obj   :: "st \<Rightarrow> val \<Rightarrow> obj"
+abbreviation val_this :: "st \<Rightarrow> val"
+  where "val_this s == the (locals s This)"
 
-translations
- "val_this s"       == "CONST the (locals s This)" 
- "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
+abbreviation lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
+  where "lookup_obj s a' == the (heap s (the_Addr a'))"
 
 subsection "memory allocation"
 
@@ -286,12 +284,8 @@
 
 subsection "initialization"
 
-syntax
-
-  init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
-
-translations
- "init_vals vs"    == "CONST Option.map default_val \<circ> vs"
+abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
+  where "init_vals vs == Option.map default_val \<circ> vs"
 
 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
 apply (unfold arr_comps_def in_bounds_def)
@@ -325,11 +319,9 @@
   init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
  "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
 
-syntax
+abbreviation
   init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
-
-translations
- "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
+  where "init_class_obj G C == init_obj G undefined (Inr C)"
 
 lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
 apply (unfold gupd_def)
@@ -513,19 +505,17 @@
 apply auto
 done
 
-syntax
+abbreviation raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "raise_if c xn == abrupt_if c (Some (Xcpt (Std xn)))"
+
+abbreviation np :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "np v == raise_if (v = Null) NullPointer"
 
-  raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
-  np       :: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
-  check_neg:: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
-  error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
-  
-translations
+abbreviation check_neg :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "check_neg i' == raise_if (the_Intg i'<0) NegArrSize"
 
- "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
- "np v"          == "raise_if (v = Null)      NullPointer"
- "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
- "error_if c e"  == "abrupt_if c (Some (Error e))"
+abbreviation error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "error_if c e == abrupt_if c (Some (Error e))"
 
 lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
 apply (simp add: abrupt_if_def)
@@ -592,22 +582,23 @@
 types
   state = "abopt \<times> st"          --{* state including abruption information *}
 
-syntax 
-  Norm   :: "st \<Rightarrow> state"
-  abrupt :: "state \<Rightarrow> abopt"
-  store  :: "state \<Rightarrow> st"
-
 translations
-   
-  "Norm s"     == "(None,s)" 
-  "abrupt"     => "fst"
-  "store"      => "snd"
   "abopt"       <= (type) "State.abrupt option"
   "abopt"       <= (type) "abrupt option"
   "state"      <= (type) "abopt \<times> State.st"
   "state"      <= (type) "abopt \<times> st"
 
+abbreviation
+  Norm :: "st \<Rightarrow> state"
+  where "Norm s == (None, s)"
 
+abbreviation (input)
+  abrupt :: "state \<Rightarrow> abopt"
+  where "abrupt == fst"
+
+abbreviation (input)
+  store :: "state \<Rightarrow> st"
+  where "store == snd"
 
 lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
 apply (erule_tac x = "(Some k,y)" in all_dupE)
@@ -683,15 +674,11 @@
 lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt s"
   by (cases s) simp
 
-syntax
+abbreviation set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
+  where "set_lvars l == supd (set_locals l)"
 
-  set_lvars     :: "locals \<Rightarrow> state \<Rightarrow> state"
-  restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
-  
-translations
-
- "set_lvars l" == "supd (set_locals l)"
- "restore_lvars s' s" == "set_lvars (locals (store s')) s"
+abbreviation restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
+  where "restore_lvars s' s == set_lvars (locals (store s')) s"
 
 lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
 apply (simp (no_asm_simp) only: split_tupled_all)
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Term.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -244,22 +244,23 @@
   "stmt"  <= (type) "Term.stmt"
   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
 
-syntax
-  
-  this    :: expr
-  LAcc    :: "vname \<Rightarrow> expr" ("!!")
-  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
-  Return  :: "expr \<Rightarrow> stmt"
-  StatRef :: "ref_ty \<Rightarrow> expr"
+abbreviation this :: expr
+  where "this == Acc (LVar This)"
+
+abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
+  where "!!v == Acc (LVar (EName (VNam v)))"
 
-translations
-  
- "this"       == "Acc (LVar This)"
- "!!v"        == "Acc (LVar (EName (VNam v)))"
- "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
- "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 
-                  --{* \tt Res := e;; Jmp Ret *}
- "StatRef rt" == "Cast (RefT rt) (Lit Null)"
+abbreviation
+  LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
+  where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
+
+abbreviation
+  Return :: "expr \<Rightarrow> stmt"
+  where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" --{* \tt Res := e;; Jmp Ret *}
+
+abbreviation
+  StatRef :: "ref_ty \<Rightarrow> expr"
+  where "StatRef rt == Cast (RefT rt) (Lit Null)"
   
 constdefs
 
@@ -275,17 +276,21 @@
   expressions, variables and expression lists into general terms.
 *}
 
-syntax 
-  expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
-  stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
-  var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
-  lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+abbreviation (input)
+  expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
+  where "\<langle>e\<rangle>\<^sub>e == In1l e"
+
+abbreviation (input)
+  stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
+  where "\<langle>c\<rangle>\<^sub>s == In1r c"
 
-translations 
-  "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
-  "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
-  "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
-  "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+  var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
+  where "\<langle>v\<rangle>\<^sub>v == In2 v"
+
+abbreviation (input)
+  lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+  where "\<langle>es\<rangle>\<^sub>l == In3 es"
 
 text {* It seems to be more elegant to have an overloaded injection like the
 following.
@@ -300,7 +305,7 @@
 @{text AxSem} don't follow this convention right now, but introduce subtle 
 syntactic sugar in the relations themselves to make a distinction on 
 expressions, statements and so on. So unfortunately you will encounter a 
-mixture of dealing with these injections. The translations above are used
+mixture of dealing with these injections. The abbreviations above are used
 as bridge between the different conventions.  
 *}
 
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Trans.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -60,13 +60,13 @@
 by (simp)
 declare the_var_AVar_def [simp del]
 
-syntax (xsymbols)
-  Ref  :: "loc \<Rightarrow> expr"
-  SKIP :: "expr"
+abbreviation
+  Ref :: "loc \<Rightarrow> expr"
+  where "Ref a == Lit (Addr a)"
 
-translations
-  "Ref a" == "Lit (Addr a)"
-  "SKIP"  == "Lit Unit"
+abbreviation
+  SKIP :: "expr"
+  where "SKIP == Lit Unit"
 
 inductive
   step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Type.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -36,17 +36,11 @@
   "ref_ty"  <= (type) "Type.ref_ty"
   "ty"      <= (type) "Type.ty"
 
-syntax
-         NT     :: "       \<spacespace> ty"
-         Iface  :: "qtname  \<Rightarrow> ty"
-         Class  :: "qtname  \<Rightarrow> ty"
-         Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
-
-translations
-        "NT"      == "RefT   NullT"
-        "Iface I" == "RefT (IfaceT I)"
-        "Class C" == "RefT (ClassT C)"
-        "T.[]"    == "RefT (ArrayT T)"
+abbreviation "NT == RefT NullT"
+abbreviation "Iface I == RefT (IfaceT I)"
+abbreviation "Class C == RefT (ClassT C)"
+abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
+  where "T.[] == RefT (ArrayT T)"
 
 constdefs
   the_Class :: "ty \<Rightarrow> qtname"
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -35,37 +35,22 @@
 (*subclseq, by translation*)                 (* subclass + identity       *)
   implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
 
-syntax
+abbreviation
+  subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
+  where "G|-I <:I1 J == (I,J) \<in> subint1 G"
 
- "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- "_subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
- (* Defined in Decl.thy:
- "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
- *)
- "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
-
-syntax (xsymbols)
+abbreviation
+  subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
+  where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
 
-  "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
-  "_subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
-  (* Defined in Decl.thy:
-\  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
-  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
-  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
-  *)
-  "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
+abbreviation
+  implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
+  where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
 
-translations
-
-        "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
-        "G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
-        (* Defined in Decl.thy:
-        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
-        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
-        *)
-        "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
+notation (xsymbols)
+  subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
+  subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
+  implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
 
 
 section "subclass and subinterface relations"
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellForm.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -2925,7 +2925,7 @@
     then show "?P m"
       by (auto simp add: permits_acc_def)
   next
-    case (Overriding new C declC newm old Sup)
+    case (Overriding new declC newm old Sup C)
     assume member_new: "G \<turnstile> new member_in C" and
                   new: "new = (declC, mdecl newm)" and
              override: "G \<turnstile> (declC, newm) overrides old" and
diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellType.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -43,11 +43,9 @@
   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
 
 
-
-syntax
+abbreviation
   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
-translations 
-  "pkg e" == "pid (cls e)"
+  where "pkg e == pid (cls e)"
 
 section "Static overloading: maximally specific methods "
 
@@ -426,29 +424,33 @@
                                          E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
 
 
-syntax (* for purely static typing *)
-  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
-  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
-  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
-  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
-  "_ty_exprs":: "env \<Rightarrow> [expr list,
-                     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+(* for purely static typing *)
+abbreviation
+  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
+
+abbreviation
+  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
+  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
+
+abbreviation
+  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+  where "E|-e:-T == E|-In1l e :: Inl T"
 
-syntax (xsymbols)
-  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
-  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
-  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
-  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
-  "_ty_exprs" :: "env \<Rightarrow> [expr list,
-                    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+abbreviation
+  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+  where "E|-e:=T == E|-In2 e :: Inl T"
 
-translations
-        "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
-        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
-        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
-        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
-        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
+abbreviation
+  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+  where "E|-e:#T == E|-In3 e :: Inr T"
 
+notation (xsymbols)
+  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
+  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
+  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
+  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
+  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
 
 declare not_None_eq [simp del] 
 declare split_if [split del] split_if_asm [split del]