modernized some syntax translations;
authorwenzelm
Mon Feb 08 21:28:27 2010 +0100 (2010-02-08)
changeset 35054a5db9779b026
parent 35053 43175817d83b
child 35060 6088dfd5f9c8
modernized some syntax translations;
src/CCL/Set.thy
src/CCL/Type.thy
src/CTT/CTT.thy
src/Cube/Cube.thy
src/FOL/IFOL.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Ring.thy
src/HOL/Auth/Message.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Union.thy
src/Sequents/ILL_predlog.thy
     1.1 --- a/src/CCL/Set.thy	Mon Feb 08 21:26:52 2010 +0100
     1.2 +++ b/src/CCL/Set.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -40,11 +40,11 @@
     1.4    "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
     1.5  
     1.6  translations
     1.7 -  "{x. P}"      == "Collect(%x. P)"
     1.8 -  "INT x:A. B"  == "INTER(A, %x. B)"
     1.9 -  "UN x:A. B"   == "UNION(A, %x. B)"
    1.10 -  "ALL x:A. P"  == "Ball(A, %x. P)"
    1.11 -  "EX x:A. P"   == "Bex(A, %x. P)"
    1.12 +  "{x. P}"      == "CONST Collect(%x. P)"
    1.13 +  "INT x:A. B"  == "CONST INTER(A, %x. B)"
    1.14 +  "UN x:A. B"   == "CONST UNION(A, %x. B)"
    1.15 +  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
    1.16 +  "EX x:A. P"   == "CONST Bex(A, %x. P)"
    1.17  
    1.18  local
    1.19  
     2.1 --- a/src/CCL/Type.thy	Mon Feb 08 21:26:52 2010 +0100
     2.2 +++ b/src/CCL/Type.thy	Mon Feb 08 21:28:27 2010 +0100
     2.3 @@ -39,15 +39,15 @@
     2.4    "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
     2.5  
     2.6  translations
     2.7 -  "PROD x:A. B" => "Pi(A, %x. B)"
     2.8 -  "A -> B"      => "Pi(A, %_. B)"
     2.9 -  "SUM x:A. B"  => "Sigma(A, %x. B)"
    2.10 -  "A * B"       => "Sigma(A, %_. B)"
    2.11 -  "{x: A. B}"   == "Subtype(A, %x. B)"
    2.12 +  "PROD x:A. B" => "CONST Pi(A, %x. B)"
    2.13 +  "A -> B"      => "CONST Pi(A, %_. B)"
    2.14 +  "SUM x:A. B"  => "CONST Sigma(A, %x. B)"
    2.15 +  "A * B"       => "CONST Sigma(A, %_. B)"
    2.16 +  "{x: A. B}"   == "CONST Subtype(A, %x. B)"
    2.17  
    2.18  print_translation {*
    2.19 -  [("Pi", dependent_tr' ("@Pi", "@->")),
    2.20 -   ("Sigma", dependent_tr' ("@Sigma", "@*"))] *}
    2.21 +  [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
    2.22 +   (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
    2.23  
    2.24  axioms
    2.25    Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
     3.1 --- a/src/CTT/CTT.thy	Mon Feb 08 21:26:52 2010 +0100
     3.2 +++ b/src/CTT/CTT.thy	Mon Feb 08 21:28:27 2010 +0100
     3.3 @@ -63,8 +63,8 @@
     3.4    "_PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
     3.5    "_SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
     3.6  translations
     3.7 -  "PROD x:A. B" == "Prod(A, %x. B)"
     3.8 -  "SUM x:A. B"  == "Sum(A, %x. B)"
     3.9 +  "PROD x:A. B" == "CONST Prod(A, %x. B)"
    3.10 +  "SUM x:A. B"  == "CONST Sum(A, %x. B)"
    3.11  
    3.12  abbreviation
    3.13    Arrow     :: "[t,t]=>t"  (infixr "-->" 30) where
     4.1 --- a/src/Cube/Cube.thy	Mon Feb 08 21:26:52 2010 +0100
     4.2 +++ b/src/Cube/Cube.thy	Mon Feb 08 21:28:27 2010 +0100
     4.3 @@ -43,9 +43,9 @@
     4.4  
     4.5  translations
     4.6    ("prop") "x:X" == ("prop") "|- x:X"
     4.7 -  "Lam x:A. B"   == "Abs(A, %x. B)"
     4.8 -  "Pi x:A. B"    => "Prod(A, %x. B)"
     4.9 -  "A -> B"       => "Prod(A, %_. B)"
    4.10 +  "Lam x:A. B"   == "CONST Abs(A, %x. B)"
    4.11 +  "Pi x:A. B"    => "CONST Prod(A, %x. B)"
    4.12 +  "A -> B"       => "CONST Prod(A, %_. B)"
    4.13  
    4.14  syntax (xsymbols)
    4.15    Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
    4.16 @@ -54,7 +54,7 @@
    4.17    Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
    4.18    arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
    4.19  
    4.20 -print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
    4.21 +print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
    4.22  
    4.23  axioms
    4.24    s_b:          "*: []"
     5.1 --- a/src/FOL/IFOL.thy	Mon Feb 08 21:26:52 2010 +0100
     5.2 +++ b/src/FOL/IFOL.thy	Mon Feb 08 21:28:27 2010 +0100
     5.3 @@ -772,7 +772,7 @@
     5.4  
     5.5  translations
     5.6    "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
     5.7 -  "let x = a in e"          == "Let(a, %x. e)"
     5.8 +  "let x = a in e"          == "CONST Let(a, %x. e)"
     5.9  
    5.10  
    5.11  lemma LetI: 
     6.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 08 21:26:52 2010 +0100
     6.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 08 21:28:27 2010 +0100
     6.3 @@ -302,7 +302,7 @@
     6.4    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     6.5        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
     6.6  translations
     6.7 -  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
     6.8 +  "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
     6.9    -- {* Beware of argument permutation! *}
    6.10  
    6.11  lemma (in comm_monoid) finprod_empty [simp]: 
     7.1 --- a/src/HOL/Algebra/Ring.thy	Mon Feb 08 21:26:52 2010 +0100
     7.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Feb 08 21:28:27 2010 +0100
     7.3 @@ -213,7 +213,7 @@
     7.4    "_finsum" :: "index => idt => 'a set => 'b => 'b"
     7.5        ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
     7.6  translations
     7.7 -  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"
     7.8 +  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
     7.9    -- {* Beware of argument permutation! *}
    7.10  
    7.11  context abelian_monoid begin
     8.1 --- a/src/HOL/Auth/Message.thy	Mon Feb 08 21:26:52 2010 +0100
     8.2 +++ b/src/HOL/Auth/Message.thy	Mon Feb 08 21:28:27 2010 +0100
     8.3 @@ -58,7 +58,7 @@
     8.4  
     8.5  translations
     8.6    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
     8.7 -  "{|x, y|}"      == "MPair x y"
     8.8 +  "{|x, y|}"      == "CONST MPair x y"
     8.9  
    8.10  
    8.11  constdefs
     9.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 21:26:52 2010 +0100
     9.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 21:28:27 2010 +0100
     9.3 @@ -15,11 +15,8 @@
     9.4  datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
     9.5    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
     9.6  
     9.7 -ML{* @{term "Add"}*}
     9.8 -syntax "_poly0" :: "poly" ("0\<^sub>p")
     9.9 -translations "0\<^sub>p" \<rightleftharpoons> "C (0\<^sub>N)"
    9.10 -syntax "_poly" :: "int \<Rightarrow> poly" ("_\<^sub>p")
    9.11 -translations "i\<^sub>p" \<rightleftharpoons> "C (i\<^sub>N)"
    9.12 +abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    9.13 +abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
    9.14  
    9.15  subsection{* Boundedness, substitution and all that *}
    9.16  consts polysize:: "poly \<Rightarrow> nat"
    9.17 @@ -117,14 +114,14 @@
    9.18    polysub :: "poly\<times>poly \<Rightarrow> poly"
    9.19    polymul :: "poly\<times>poly \<Rightarrow> poly"
    9.20    polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
    9.21 -syntax "_polyadd" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
    9.22 -translations "a +\<^sub>p b" \<rightleftharpoons> "polyadd (a,b)"  
    9.23 -syntax "_polymul" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    9.24 -translations "a *\<^sub>p b" \<rightleftharpoons> "polymul (a,b)"  
    9.25 -syntax "_polysub" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
    9.26 -translations "a -\<^sub>p b" \<rightleftharpoons> "polysub (a,b)"  
    9.27 -syntax "_polypow" :: "nat \<Rightarrow> poly \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
    9.28 -translations "a ^\<^sub>p k" \<rightleftharpoons> "polypow k a" 
    9.29 +abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
    9.30 +  where "a +\<^sub>p b \<equiv> polyadd (a,b)"
    9.31 +abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    9.32 +  where "a *\<^sub>p b \<equiv> polymul (a,b)"
    9.33 +abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
    9.34 +  where "a -\<^sub>p b \<equiv> polysub (a,b)"
    9.35 +abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
    9.36 +  where "a ^\<^sub>p k \<equiv> polypow k a"
    9.37  
    9.38  recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
    9.39    "polyadd (C c, C c') = C (c+\<^sub>Nc')"
    9.40 @@ -243,8 +240,9 @@
    9.41    "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
    9.42    "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
    9.43    "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
    9.44 -syntax "_Ipoly" :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    9.45 -translations "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup>" \<rightleftharpoons> "Ipoly bs p"  
    9.46 +abbreviation
    9.47 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    9.48 +  where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    9.49  
    9.50  lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
    9.51    by (simp add: INum_def)
    10.1 --- a/src/HOL/Hoare/Hoare.thy	Mon Feb 08 21:26:52 2010 +0100
    10.2 +++ b/src/HOL/Hoare/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
    10.3 @@ -24,12 +24,7 @@
    10.4     | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    10.5     | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    10.6    
    10.7 -syntax
    10.8 -  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
    10.9 -  "@annskip" :: "'a com"                    ("SKIP")
   10.10 -
   10.11 -translations
   10.12 -            "SKIP" == "Basic id"
   10.13 +abbreviation annskip ("SKIP") where "SKIP == Basic id"
   10.14  
   10.15  types 'a sem = "'a => 'a => bool"
   10.16  
   10.17 @@ -50,16 +45,19 @@
   10.18    "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
   10.19  
   10.20  
   10.21 -syntax
   10.22 - "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
   10.23 -                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
   10.24 -syntax ("" output)
   10.25 - "@hoare"      :: "['a assn,'a com,'a assn] => bool"
   10.26 -                 ("{_} // _ // {_}" [0,55,0] 50)
   10.27  
   10.28  (** parse translations **)
   10.29  
   10.30 -ML{*
   10.31 +syntax
   10.32 +  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
   10.33 +
   10.34 +syntax
   10.35 + "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
   10.36 +                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
   10.37 +syntax ("" output)
   10.38 + "_hoare"      :: "['a assn,'a com,'a assn] => bool"
   10.39 +                 ("{_} // _ // {_}" [0,55,0] 50)
   10.40 +ML {*
   10.41  
   10.42  local
   10.43  
   10.44 @@ -91,7 +89,7 @@
   10.45  *}
   10.46  (* com_tr *)
   10.47  ML{*
   10.48 -fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
   10.49 +fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
   10.50        Syntax.const "Basic" $ mk_fexp a e xs
   10.51    | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
   10.52    | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
   10.53 @@ -123,7 +121,7 @@
   10.54  end
   10.55  *}
   10.56  
   10.57 -parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
   10.58 +parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
   10.59  
   10.60  
   10.61  (*****************************************************************************)
   10.62 @@ -175,8 +173,8 @@
   10.63  fun mk_assign f =
   10.64    let val (vs, ts) = mk_vts f;
   10.65        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
   10.66 -  in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
   10.67 -     else Syntax.const "@skip" end;
   10.68 +  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
   10.69 +     else Syntax.const @{const_syntax annskip} end;
   10.70  
   10.71  fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
   10.72                                             else Syntax.const "Basic" $ f
   10.73 @@ -190,10 +188,10 @@
   10.74  
   10.75  
   10.76  fun spec_tr' [p, c, q] =
   10.77 -  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   10.78 +  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   10.79  *}
   10.80  
   10.81 -print_translation {* [("Valid", spec_tr')] *}
   10.82 +print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
   10.83  
   10.84  lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   10.85  by (auto simp:Valid_def)
    11.1 --- a/src/HOL/Hoare/HoareAbort.thy	Mon Feb 08 21:26:52 2010 +0100
    11.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Mon Feb 08 21:28:27 2010 +0100
    11.3 @@ -21,12 +21,7 @@
    11.4     | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    11.5     | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    11.6    
    11.7 -syntax
    11.8 -  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
    11.9 -  "@annskip" :: "'a com"                    ("SKIP")
   11.10 -
   11.11 -translations
   11.12 -            "SKIP" == "Basic id"
   11.13 +abbreviation annskip ("SKIP") where "SKIP == Basic id"
   11.14  
   11.15  types 'a sem = "'a option => 'a option => bool"
   11.16  
   11.17 @@ -51,16 +46,19 @@
   11.18    "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
   11.19  
   11.20  
   11.21 -syntax
   11.22 - "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
   11.23 -                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
   11.24 -syntax ("" output)
   11.25 - "@hoare"      :: "['a assn,'a com,'a assn] => bool"
   11.26 -                 ("{_} // _ // {_}" [0,55,0] 50)
   11.27  
   11.28  (** parse translations **)
   11.29  
   11.30 -ML{*
   11.31 +syntax
   11.32 +  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
   11.33 +
   11.34 +syntax
   11.35 +  "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
   11.36 +                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
   11.37 +syntax ("" output)
   11.38 +  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
   11.39 +                 ("{_} // _ // {_}" [0,55,0] 50)
   11.40 +ML {*
   11.41  
   11.42  local
   11.43  fun free a = Free(a,dummyT)
   11.44 @@ -92,7 +90,7 @@
   11.45  *}
   11.46  (* com_tr *)
   11.47  ML{*
   11.48 -fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
   11.49 +fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
   11.50        Syntax.const "Basic" $ mk_fexp a e xs
   11.51    | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
   11.52    | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
   11.53 @@ -124,7 +122,7 @@
   11.54  end
   11.55  *}
   11.56  
   11.57 -parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
   11.58 +parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
   11.59  
   11.60  
   11.61  (*****************************************************************************)
   11.62 @@ -176,8 +174,8 @@
   11.63  fun mk_assign f =
   11.64    let val (vs, ts) = mk_vts f;
   11.65        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
   11.66 -  in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
   11.67 -     else Syntax.const "@skip" end;
   11.68 +  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
   11.69 +     else Syntax.const @{const_syntax annskip} end;
   11.70  
   11.71  fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
   11.72                                             else Syntax.const "Basic" $ f
   11.73 @@ -191,10 +189,10 @@
   11.74  
   11.75  
   11.76  fun spec_tr' [p, c, q] =
   11.77 -  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   11.78 +  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   11.79  *}
   11.80  
   11.81 -print_translation {* [("Valid", spec_tr')] *}
   11.82 +print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
   11.83  
   11.84  (*** The proof rules ***)
   11.85  
   11.86 @@ -257,7 +255,7 @@
   11.87  
   11.88  syntax
   11.89    guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   11.90 -  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
   11.91 +  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
   11.92  translations
   11.93    "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
   11.94    "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
    12.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Mon Feb 08 21:26:52 2010 +0100
    12.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
    12.3 @@ -228,11 +228,11 @@
    12.4    "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
    12.5  
    12.6  translations
    12.7 -  ".{b}."                   => "Collect .(b)."
    12.8 +  ".{b}."                   => "CONST Collect .(b)."
    12.9    "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
   12.10 -  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
   12.11 -  "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
   12.12 -  "WHILE b INV i DO c OD"   => "While .{b}. i c"
   12.13 +  "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
   12.14 +  "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
   12.15 +  "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"
   12.16    "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
   12.17  
   12.18  parse_translation {*
    13.1 --- a/src/HOL/Metis_Examples/Message.thy	Mon Feb 08 21:26:52 2010 +0100
    13.2 +++ b/src/HOL/Metis_Examples/Message.thy	Mon Feb 08 21:28:27 2010 +0100
    13.3 @@ -52,7 +52,7 @@
    13.4  
    13.5  translations
    13.6    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    13.7 -  "{|x, y|}"      == "MPair x y"
    13.8 +  "{|x, y|}"      == "CONST MPair x y"
    13.9  
   13.10  
   13.11  constdefs
    14.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:26:52 2010 +0100
    14.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:28:27 2010 +0100
    14.3 @@ -78,11 +78,9 @@
    14.4            {S. S \<subseteq> pset cl &
    14.5             (| pset = S, order = induced S (order cl) |): CompleteLattice }"
    14.6  
    14.7 -syntax
    14.8 -  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
    14.9 -
   14.10 -translations
   14.11 -  "S <<= cl" == "S : sublattice `` {cl}"
   14.12 +abbreviation
   14.13 +  sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
   14.14 +  where "S <<= cl \<equiv> S : sublattice `` {cl}"
   14.15  
   14.16  constdefs
   14.17    dual :: "'a potype => 'a potype"
    15.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Feb 08 21:26:52 2010 +0100
    15.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Feb 08 21:28:27 2010 +0100
    15.3 @@ -76,7 +76,7 @@
    15.4        ("(3PROD _:#_. _)" [0, 51, 10] 10)
    15.5  
    15.6  translations
    15.7 -  "PROD i :# A. b" == "msetprod (%i. b) A"
    15.8 +  "PROD i :# A. b" == "CONST msetprod (%i. b) A"
    15.9  
   15.10  lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
   15.11    apply (simp add: msetprod_def power_add)
    16.1 --- a/src/HOL/UNITY/PPROD.thy	Mon Feb 08 21:26:52 2010 +0100
    16.2 +++ b/src/HOL/UNITY/PPROD.thy	Mon Feb 08 21:28:27 2010 +0100
    16.3 @@ -11,17 +11,14 @@
    16.4  theory PPROD imports Lift_prog begin
    16.5  
    16.6  constdefs
    16.7 -
    16.8    PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
    16.9              => ((nat=>'b) * 'c) program"
   16.10      "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
   16.11  
   16.12  syntax
   16.13 -  "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
   16.14 -              ("(3plam _:_./ _)" 10)
   16.15 -
   16.16 +  "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
   16.17  translations
   16.18 -  "plam x : A. B"   == "PLam A (%x. B)"
   16.19 +  "plam x : A. B" == "CONST PLam A (%x. B)"
   16.20  
   16.21  
   16.22  (*** Basic properties ***)
    17.1 --- a/src/HOL/UNITY/Union.thy	Mon Feb 08 21:26:52 2010 +0100
    17.2 +++ b/src/HOL/UNITY/Union.thy	Mon Feb 08 21:28:27 2010 +0100
    17.3 @@ -36,19 +36,19 @@
    17.4      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    17.5  
    17.6  syntax
    17.7 -  "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
    17.8 -  "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
    17.9 +  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   17.10 +  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
   17.11  
   17.12  translations
   17.13 -  "JN x : A. B"   == "JOIN A (%x. B)"
   17.14 -  "JN x y. B"   == "JN x. JN y. B"
   17.15 -  "JN x. B"     == "JOIN CONST UNIV (%x. B)"
   17.16 +  "JN x: A. B" == "CONST JOIN A (%x. B)"
   17.17 +  "JN x y. B" == "JN x. JN y. B"
   17.18 +  "JN x. B" == "JOIN CONST UNIV (%x. B)"
   17.19  
   17.20  syntax (xsymbols)
   17.21    SKIP     :: "'a program"                              ("\<bottom>")
   17.22    Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
   17.23 -  "@JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
   17.24 -  "@JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
   17.25 +  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
   17.26 +  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
   17.27  
   17.28  
   17.29  subsection{*SKIP*}
    18.1 --- a/src/Sequents/ILL_predlog.thy	Mon Feb 08 21:26:52 2010 +0100
    18.2 +++ b/src/Sequents/ILL_predlog.thy	Mon Feb 08 21:28:27 2010 +0100
    18.3 @@ -22,8 +22,8 @@
    18.4  
    18.5    "[* A & B *]" == "[*A*] && [*B*]"
    18.6    "[* A | B *]" == "![*A*] ++ ![*B*]"
    18.7 -  "[* - A *]"   == "[*A > ff*]"
    18.8 -  "[* ff *]"    == "0"
    18.9 +  "[* - A *]"   == "[*A > CONST ff*]"
   18.10 +  "[* XCONST ff *]" == "0"
   18.11    "[* A = B *]" => "[* (A > B) & (B > A) *]"
   18.12  
   18.13    "[* A > B *]" == "![*A*] -o [*B*]"