# HG changeset patch
# User wenzelm
# Date 1265845502 -3600
# Node ID cc7a0b9f938cd3795d38356dada45d813a1354cd
# Parent  6ce9177d6b38a84f6a28d8038aa7996a7120f0f9
modernized translations;

diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -296,12 +296,10 @@
   done
 
 text {* Some abbreviations for readability *} 
-syntax
-  Clist :: ty 
-  Ctest :: ty
-translations
-  "Clist" == "Class list_name"
-  "Ctest" == "Class test_name"
+abbreviation Clist :: ty 
+  where "Clist == Class list_name"
+abbreviation Ctest :: ty
+  where "Ctest == Class test_name"
 
 constdefs
   phi_makelist :: method_type ("\<phi>\<^sub>m")
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -37,9 +37,7 @@
   "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
                (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)"
 
-
-translations
-  "types G" == "Collect (is_type G)"
+abbreviation "types G == Collect (is_type G)"
 
 constdefs
   esl :: "'c prog \<Rightarrow> ty esl"
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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>
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -262,10 +262,8 @@
 done
 
 
-syntax
-  mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c"
-translations
-  "mtd_mb" => "Fun.comp snd snd"
+abbreviation (input)
+  "mtd_mb == snd o snd"
 
 lemma map_of_map_fst: "\<lbrakk> inj f;
   \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/Comp/TranslCompTp.thy
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -41,13 +41,13 @@
 
 (**********************************************************************)
 
-syntax
-  mt_of         :: "method_type \<times> state_type \<Rightarrow> method_type"
-  sttp_of       :: "method_type \<times> state_type \<Rightarrow> state_type"
+abbreviation (input)
+  mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
+  where "mt_of == fst"
 
-translations
-  "mt_of"     => "fst"
-  "sttp_of"   => "snd"
+abbreviation (input)
+  sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
+  where "sttp_of == snd"
 
 consts
   compTpExpr  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
@@ -189,4 +189,3 @@
 
 
 end
-
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -45,10 +45,9 @@
  sl :: "'a esl \<Rightarrow> 'a err sl"
 "sl == %(A,r,f). (err A, le r, lift2 f)"
 
-syntax
- err_semilat :: "'a esl \<Rightarrow> bool"
-translations
-"err_semilat L" == "semilat(Err.sl L)"
+abbreviation
+  err_semilat :: "'a esl \<Rightarrow> bool"
+  where "err_semilat L == semilat(Err.sl L)"
 
 
 consts
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -17,21 +17,24 @@
  le :: "'a ord \<Rightarrow> ('a list)ord"
 "le r == list_all2 (%x y. x <=_r y)"
 
-syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+abbreviation
+  lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
        ("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "x <=[r] y == x <=_(le r) y"
+
+abbreviation
+  lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
        ("(_ /<[_] _)" [50, 0, 51] 50)
-translations
- "x <=[r] y" == "x <=_(Listn.le r) y"
- "x <[r] y"  == "x <_(Listn.le r) y"
+  where "x <[r] y == x <_(le r) y"
 
 constdefs
  map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
 "map2 f == (%xs ys. map (split f) (zip xs ys))"
 
-syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
+abbreviation
+  plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
        ("(_ /+[_] _)" [65, 0, 66] 65)
-translations  "x +[f] y" == "x +_(map2 f) y"
+  where "x +[f] y == x +_(map2 f) y"
 
 consts coalesce :: "'a err list \<Rightarrow> 'a list err"
 primrec
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/J/Example.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -55,19 +54,16 @@
 
 declare inj_cnam' [simp] inj_vnam' [simp]
 
-syntax
-  Base :: cname
-  Ext  :: cname
-  vee  :: vname
-  x    :: vname
-  e    :: vname
-
-translations
-  "Base" == "cnam' Base'"
-  "Ext"  == "cnam' Ext'"
-  "vee"  == "VName (vnam' vee')"
-  "x"  == "VName (vnam' x')"
-  "e"  == "VName (vnam' e')"
+abbreviation Base :: cname
+  where "Base == cnam' Base'"
+abbreviation Ext :: cname
+  where "Ext == cnam' Ext'"
+abbreviation vee :: vname
+  where "vee == VName (vnam' vee')"
+abbreviation x :: vname
+  where "x == VName (vnam' x')"
+abbreviation e :: vname
+  where "e == VName (vnam' e')"
 
 axioms
   Base_not_Object: "Base \<noteq> Object"
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/J/Exceptions.thy
--- a/src/HOL/MicroJava/J/Exceptions.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/J/Exceptions.thy
-    ID:         $Id$
     Author:     Gerwin Klein, Martin Strecker
     Copyright   2002 Technische Universitaet Muenchen
 *)
@@ -17,11 +16,9 @@
                         (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
 
 
-consts
+abbreviation
   cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
-
-translations
-  "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))"
+  where "cname_of hp v == fst (the (hp (the_Addr v)))"
 
 
 constdefs
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/State.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -27,21 +27,27 @@
       state  = "aheap \<times> locals"      -- "heap, local parameter including This"
       xstate = "val option \<times> state" -- "state including exception information"
 
-syntax
-  heap    :: "state => aheap"
-  locals  :: "state => locals"
-  Norm    :: "state => xstate"
-  abrupt  :: "xstate \<Rightarrow> val option"
-  store   :: "xstate \<Rightarrow> state"
-  lookup_obj   :: "state \<Rightarrow> val \<Rightarrow> obj"
+abbreviation (input)
+  heap :: "state => aheap"
+  where "heap == fst"
+
+abbreviation (input)
+  locals :: "state => locals"
+  where "locals == snd"
+
+abbreviation "Norm s == (None, s)"
 
-translations
-  "heap"   => "fst"
-  "locals" => "snd"
-  "Norm s" == "(None,s)"
-  "abrupt"     => "fst"
-  "store"      => "snd"
- "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
+abbreviation (input)
+  abrupt :: "xstate \<Rightarrow> val option"
+  where "abrupt == fst"
+
+abbreviation (input)
+  store :: "xstate \<Rightarrow> state"
+  where "store == snd"
+
+abbreviation
+  lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+  where "lookup_obj s a' == the (heap s (the_Addr a'))"
 
 
 constdefs
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/J/Type.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -47,12 +46,10 @@
   = PrimT prim_ty -- "primitive type"
   | RefT  ref_ty  -- "reference type"
 
-syntax
-  NT    :: "ty"
-  Class :: "cname  => ty"
+abbreviation NT :: ty
+  where "NT == RefT NullT"
 
-translations
-  "NT"      == "RefT NullT"
-  "Class C" == "RefT (ClassT C)"
+abbreviation Class :: "cname  => ty"
+  where "Class C == RefT (ClassT C)"
 
 end
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/J/WellType.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -27,13 +26,13 @@
   lenv   = "vname \<rightharpoonup> ty"
   'c env = "'c prog \<times> lenv"
 
-syntax
-  prg    :: "'c env => 'c prog"
-  localT :: "'c env => (vname \<rightharpoonup> ty)"
+abbreviation (input)
+  prg :: "'c env => 'c prog"
+  where "prg == fst"
 
-translations  
-  "prg"    => "fst"
-  "localT" => "snd"
+abbreviation (input)
+  localT :: "'c env => (vname \<rightharpoonup> ty)"
+  where "localT == snd"
 
 consts
   more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
@@ -207,10 +206,7 @@
   (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
    E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
 
-syntax 
- wf_java_prog :: "'c prog => bool"
-translations
-  "wf_java_prog" == "wf_prog wf_java_mdecl"
+abbreviation "wf_java_prog == wf_prog wf_java_mdecl"
 
 lemma wf_java_prog_wf_java_mdecl: "\<lbrakk> 
   wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
-    ID:         $Id$
     Author:     Gerwin Klein
 *)
 
@@ -13,9 +12,9 @@
 datatype 'a type_error = TypeError | Normal 'a
 
 
-syntax "fifth" :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
-translations
-  "fifth x" == "fst(snd(snd(snd(snd x))))"
+abbreviation
+  fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
+  where "fifth x == fst(snd(snd(snd(snd x))))"
 
 
 consts isAddr :: "val \<Rightarrow> bool"
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
-    ID:         $Id$
     Author:     Gerwin Klein, Martin Strecker
     Copyright   2001 Technische Universitaet Muenchen
 *)
@@ -24,10 +23,9 @@
                                            then Some (fst (snd (snd e))) 
                                            else match_exception_table G cn pc es)"
 
-consts
+abbreviation
   ex_table_of :: "jvm_method \<Rightarrow> exception_table"
-translations
-  "ex_table_of m" == "snd (snd (snd m))"
+  where "ex_table_of m == snd (snd (snd m))"
 
 
 consts
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/Example.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -50,11 +50,14 @@
 consts suc  :: mname
        add  :: mname
 consts any  :: vname
-syntax dummy:: expr ("<>")
-       one  :: expr
-translations 
-      "<>"  == "LAcc any"
-      "one" == "{Nat}new Nat..suc(<>)"
+
+abbreviation
+  dummy :: expr ("<>")
+  where "<> == LAcc any"
+
+abbreviation
+  one :: expr
+  where "one == {Nat}new Nat..suc(<>)"
 
 text {* The following properties could be derived from a more complete
         program model, which we leave out for laziness. *}
diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -11,16 +11,16 @@
 consts
   subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
 
-syntax (xsymbols)
-  subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
-  subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
-syntax
-  subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
-  subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
+abbreviation
+  subcls1_syntax :: "[cname, cname] => bool"  ("_ <=C1 _" [71,71] 70)
+  where "C <=C1 D == (C,D) \<in> subcls1"
+abbreviation
+  subcls_syntax  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
+  where "C <=C D == (C,D) \<in> subcls1^*"
 
-translations
-  "C \<prec>C1 D" == "(C,D) \<in> subcls1"
-  "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
+notation (xsymbols)
+  subcls1_syntax  ("_ \<prec>C1 _"  [71,71] 70) and
+  subcls_syntax  ("_ \<preceq>C _"   [71,71] 70)
 
 consts
   method :: "cname => (mname \<rightharpoonup> methd)"