refined 'abbreviation';
authorwenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363667b5ea637dd
parent 19362 638bbd5a4a3b
child 19364 38799cfa34e5
refined 'abbreviation';
NEWS
doc-src/IsarRef/generic.tex
src/FOL/IFOL.thy
src/HOL/Auth/Guard/Guard_Shared.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Infinite_Set.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Accessible_Part.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Unix/Unix.thy
src/HOL/ex/Abstract_NAT.thy
src/HOL/ex/Classpackage.thy
     1.1 --- a/NEWS	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/NEWS	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -144,9 +144,9 @@
     1.4      eq  (infix "===" 50)
     1.5      where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
     1.6  
     1.7 -  abbreviation (output)
     1.8 +  abbreviation
     1.9      neq  (infix "=!=" 50)
    1.10 -    "(x =!= y) <-> ~ (x === y)"
    1.11 +    "x =!= y == ~ (x === y)"
    1.12  
    1.13  These specifications may be also used in a locale context.  Then the
    1.14  constants being introduced depend on certain fixed parameters, and the
    1.15 @@ -157,10 +157,9 @@
    1.16  entities from a monomorphic theory.
    1.17  
    1.18  Presently, abbreviations are only available 'in' a target locale, but
    1.19 -not inherited by general import expressions.
    1.20 -
    1.21 -Also note that 'abbreviation' may be used as a type-safe replacement
    1.22 -for 'syntax' + 'translations' in common applications.
    1.23 +not inherited by general import expressions.  Also note that
    1.24 +'abbreviation' may be used as a type-safe replacement for 'syntax' +
    1.25 +'translations' in common applications.
    1.26  
    1.27  * Provers/induct: improved internal context management to support
    1.28  local fixes and defines on-the-fly.  Thus explicit meta-level
     2.1 --- a/doc-src/IsarRef/generic.tex	Sat Apr 08 22:12:02 2006 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Sat Apr 08 22:51:06 2006 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    'definition' locale? (constdecl? constdef +)
     2.5    ;
     2.6  
     2.7 -  'abbreviation' locale? '(output)'? (constdecl? prop +)
     2.8 +  'abbreviation' locale? mode? (constdecl? prop +)
     2.9    ;
    2.10    'axiomatization' locale? consts? ('where' specs)?
    2.11    ;
    2.12 @@ -55,16 +55,20 @@
    2.13    supported here.
    2.14    
    2.15  \item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
    2.16 -  a syntactic constant which is associated with a certain term derived
    2.17 -  from the specification given as $eq$.  The very same transformations
    2.18 -  as for $\isarkeyword{definition}$ are applied here, although
    2.19 -  additional conditions are not supported.
    2.20 +  a syntactic constant which is associated with a certain term
    2.21 +  according to the meta-level equality $eq$.
    2.22    
    2.23    Abbreviations participate in the usual type-inference process, but
    2.24 -  are expanded before the logic ever sees them.  The expansion is
    2.25 -  one-way by default; the ``$(output)$'' option makes abbreviations
    2.26 -  fold back whenever terms are pretty printed.  The latter needs some
    2.27 -  care to avoid overlapping or looping syntactic replacements!
    2.28 +  are expanded before the logic ever sees them.  Pretty printing of
    2.29 +  terms involves higher-order rewriting with rules stemming from
    2.30 +  reverted abbreviations.  This needs some care to avoid overlapping
    2.31 +  or looping syntactic replacements!
    2.32 +  
    2.33 +  The optional $mode$ specification restricts output to a particular
    2.34 +  print mode; using ``$input$'' here achieves the effect of one-way
    2.35 +  abbreviations.  The mode may also include an ``$output$'' qualifier
    2.36 +  that affects the concrete syntax declared for abbreviations, cf.\ 
    2.37 +  $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
    2.38    
    2.39  \item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
    2.40    \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
     3.1 --- a/src/FOL/IFOL.thy	Sat Apr 08 22:12:02 2006 +0200
     3.2 +++ b/src/FOL/IFOL.thy	Sat Apr 08 22:51:06 2006 +0200
     3.3 @@ -45,10 +45,18 @@
     3.4    Ex1           :: "('a => o) => o"             (binder "EX! " 10)
     3.5  
     3.6  
     3.7 -abbreviation (output)
     3.8 +abbreviation
     3.9    not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
    3.10    "x ~= y == ~ (x = y)"
    3.11  
    3.12 +abbreviation (xsymbols)
    3.13 +  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    3.14 +  "x \<noteq> y == ~ (x = y)"
    3.15 +
    3.16 +abbreviation (HTML output)
    3.17 +  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    3.18 +  "not_equal == xsymbols.not_equal"
    3.19 +
    3.20  syntax (xsymbols)
    3.21    Not           :: "o => o"                     ("\<not> _" [40] 40)
    3.22    "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    3.23 @@ -56,7 +64,6 @@
    3.24    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    3.25    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    3.26    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    3.27 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    3.28    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    3.29    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    3.30  
    3.31 @@ -67,7 +74,6 @@
    3.32    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    3.33    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    3.34    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    3.35 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    3.36  
    3.37  
    3.38  local
     4.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:12:02 2006 +0200
     4.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:51:06 2006 +0200
     4.3 @@ -19,9 +19,9 @@
     4.4  
     4.5  subsubsection{*a little abbreviation*}
     4.6  
     4.7 -syntax Ciph :: "agent => msg"
     4.8 -
     4.9 -translations "Ciph A X" == "Crypt (shrK A) X"
    4.10 +abbreviation
    4.11 +  Ciph :: "agent => msg => msg"
    4.12 +  "Ciph A X == Crypt (shrK A) X"
    4.13  
    4.14  subsubsection{*agent associated to a key*}
    4.15  
     5.1 --- a/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:12:02 2006 +0200
     5.2 +++ b/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:51:06 2006 +0200
     5.3 @@ -163,9 +163,9 @@
     5.4    fixes r and f
     5.5    assumes congruent: "(y,z) \<in> r ==> f y = f z"
     5.6  
     5.7 -abbreviation (output)
     5.8 +abbreviation
     5.9    RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
    5.10 -  "f respects r = congruent r f"
    5.11 +  "f respects r == congruent r f"
    5.12  
    5.13  
    5.14  lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
     6.1 --- a/src/HOL/Finite_Set.thy	Sat Apr 08 22:12:02 2006 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Sat Apr 08 22:51:06 2006 +0200
     6.3 @@ -13,8 +13,8 @@
     6.4  subsection {* Definition and basic properties *}
     6.5  
     6.6  consts Finites :: "'a set set"
     6.7 -abbreviation (output)
     6.8 -  "finite A = (A : Finites)"
     6.9 +abbreviation
    6.10 +  "finite A == A : Finites"
    6.11  
    6.12  inductive Finites
    6.13    intros
     7.1 --- a/src/HOL/Fun.thy	Sat Apr 08 22:12:02 2006 +0200
     7.2 +++ b/src/HOL/Fun.thy	Sat Apr 08 22:51:06 2006 +0200
     7.3 @@ -59,19 +59,19 @@
     7.4  
     7.5  constdefs
     7.6    inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
     7.7 -    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     7.8 +  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     7.9  
    7.10  text{*A common special case: functions injective over the entire domain type.*}
    7.11  
    7.12 -abbreviation (output)
    7.13 -  "inj f = inj_on f UNIV"
    7.14 +abbreviation
    7.15 +  "inj f == inj_on f UNIV"
    7.16  
    7.17  constdefs
    7.18    surj :: "('a => 'b) => bool"                   (*surjective*)
    7.19 -    "surj f == ! y. ? x. y=f(x)"
    7.20 +  "surj f == ! y. ? x. y=f(x)"
    7.21  
    7.22    bij :: "('a => 'b) => bool"                    (*bijective*)
    7.23 -    "bij f == inj f & surj f"
    7.24 +  "bij f == inj f & surj f"
    7.25  
    7.26  
    7.27  
     8.1 --- a/src/HOL/Infinite_Set.thy	Sat Apr 08 22:12:02 2006 +0200
     8.2 +++ b/src/HOL/Infinite_Set.thy	Sat Apr 08 22:51:06 2006 +0200
     8.3 @@ -13,12 +13,9 @@
     8.4  
     8.5  text {* Some elementary facts about infinite sets, by Stefan Merz. *}
     8.6  
     8.7 -syntax infinite :: "'a set \<Rightarrow> bool"
     8.8 -translations "infinite S" == "\<not> finite S"
     8.9 -(* doesnt work:
    8.10 -abbreviation (output)
    8.11 -  "infinite S = (\<not> finite S)"
    8.12 -*)
    8.13 +abbreviation
    8.14 +  infinite :: "'a set \<Rightarrow> bool"
    8.15 +  "infinite S == \<not> finite S"
    8.16  
    8.17  text {*
    8.18    Infinite sets are non-empty, and if we remove some elements
     9.1 --- a/src/HOL/Isar_examples/Hoare.thy	Sat Apr 08 22:12:02 2006 +0200
     9.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Sat Apr 08 22:51:06 2006 +0200
     9.3 @@ -31,7 +31,7 @@
     9.4    | Cond "'a bexp" "'a com" "'a com"
     9.5    | While "'a bexp" "'a assn" "'a com"
     9.6  
     9.7 -abbreviation (output)
     9.8 +abbreviation
     9.9    Skip  ("SKIP")
    9.10    "SKIP == Basic id"
    9.11  
    10.1 --- a/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:12:02 2006 +0200
    10.2 +++ b/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:51:06 2006 +0200
    10.3 @@ -25,9 +25,9 @@
    10.4    "Church_Rosser R =
    10.5      (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
    10.6  
    10.7 -abbreviation (output)
    10.8 +abbreviation
    10.9    confluent :: "('a \<times> 'a) set => bool"
   10.10 -  "confluent R = diamond (R^*)"
   10.11 +  "confluent R == diamond (R^*)"
   10.12  
   10.13  
   10.14  subsection {* Basic lemmas *}
    11.1 --- a/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:12:02 2006 +0200
    11.2 +++ b/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:51:06 2006 +0200
    11.3 @@ -21,13 +21,13 @@
    11.4  consts
    11.5    eta :: "(dB \<times> dB) set"
    11.6  
    11.7 -abbreviation (output)
    11.8 +abbreviation
    11.9    eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
   11.10 -  "(s -e> t) = ((s, t) \<in> eta)"
   11.11 +  "s -e> t == (s, t) \<in> eta"
   11.12    eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
   11.13 -  "(s -e>> t) = ((s, t) \<in> eta^*)"
   11.14 +  "s -e>> t == (s, t) \<in> eta^*"
   11.15    eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
   11.16 -  "(s -e>= t) = ((s, t) \<in> eta^=)"
   11.17 +  "s -e>= t == (s, t) \<in> eta^="
   11.18  
   11.19  inductive eta
   11.20    intros
   11.21 @@ -224,12 +224,13 @@
   11.22  consts
   11.23    par_eta :: "(dB \<times> dB) set"
   11.24  
   11.25 -abbreviation (output)
   11.26 +abbreviation
   11.27    par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
   11.28 -  "(s =e> t) = ((s, t) \<in> par_eta)"
   11.29 +  "s =e> t == (s, t) \<in> par_eta"
   11.30  
   11.31 -syntax (xsymbols)
   11.32 +abbreviation (xsymbols)
   11.33    par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
   11.34 +  "op \<Rightarrow>\<^sub>\<eta> == op =e>"
   11.35  
   11.36  inductive par_eta
   11.37  intros
    12.1 --- a/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:12:02 2006 +0200
    12.2 +++ b/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:51:06 2006 +0200
    12.3 @@ -56,15 +56,17 @@
    12.4  consts
    12.5    beta :: "(dB \<times> dB) set"
    12.6  
    12.7 -abbreviation (output)
    12.8 +abbreviation
    12.9    beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
   12.10 -  "(s -> t) = ((s, t) \<in> beta)"
   12.11 +  "s -> t == (s, t) \<in> beta"
   12.12    beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
   12.13 -  "(s ->> t) = ((s, t) \<in> beta^*)"
   12.14 +  "s ->> t == (s, t) \<in> beta^*"
   12.15  
   12.16 -syntax (latex)
   12.17 +abbreviation (latex)
   12.18    beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   12.19 +  "op \<rightarrow>\<^sub>\<beta> == op ->"
   12.20    beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
   12.21 +  "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
   12.22  
   12.23  inductive beta
   12.24    intros
    13.1 --- a/src/HOL/Lambda/ListApplication.thy	Sat Apr 08 22:12:02 2006 +0200
    13.2 +++ b/src/HOL/Lambda/ListApplication.thy	Sat Apr 08 22:51:06 2006 +0200
    13.3 @@ -8,9 +8,9 @@
    13.4  
    13.5  theory ListApplication imports Lambda begin
    13.6  
    13.7 -abbreviation (output)
    13.8 +abbreviation
    13.9    list_application :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
   13.10 -  "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
   13.11 +  "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
   13.12  
   13.13  lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
   13.14    by (induct ts rule: rev_induct) auto
    14.1 --- a/src/HOL/Lambda/ListBeta.thy	Sat Apr 08 22:12:02 2006 +0200
    14.2 +++ b/src/HOL/Lambda/ListBeta.thy	Sat Apr 08 22:51:06 2006 +0200
    14.3 @@ -12,9 +12,9 @@
    14.4    Lifting beta-reduction to lists of terms, reducing exactly one element.
    14.5  *}
    14.6  
    14.7 -abbreviation (output)
    14.8 +abbreviation
    14.9    list_beta :: "dB list => dB list => bool"   (infixl "=>" 50)
   14.10 -  "(rs => ss) = ((rs, ss) : step1 beta)"
   14.11 +  "rs => ss == (rs, ss) : step1 beta"
   14.12  
   14.13  lemma head_Var_reduction:
   14.14    "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
    15.1 --- a/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:12:02 2006 +0200
    15.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:51:06 2006 +0200
    15.3 @@ -17,9 +17,9 @@
    15.4  consts
    15.5    par_beta :: "(dB \<times> dB) set"
    15.6  
    15.7 -abbreviation (output)
    15.8 +abbreviation
    15.9    par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
   15.10 -  "(s => t) = ((s, t) \<in> par_beta)"
   15.11 +  "s => t == (s, t) \<in> par_beta"
   15.12  
   15.13  inductive par_beta
   15.14    intros
    16.1 --- a/src/HOL/Lambda/Type.thy	Sat Apr 08 22:12:02 2006 +0200
    16.2 +++ b/src/HOL/Lambda/Type.thy	Sat Apr 08 22:51:06 2006 +0200
    16.3 @@ -14,10 +14,14 @@
    16.4  definition
    16.5    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
    16.6    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
    16.7 -syntax (xsymbols)
    16.8 -  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    16.9 -syntax (HTML output)
   16.10 -  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   16.11 +
   16.12 +abbreviation (xsymbols)
   16.13 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   16.14 +  "e\<langle>i:a\<rangle> == e<i:a>"
   16.15 +
   16.16 +abbreviation (HTML output)
   16.17 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   16.18 +  "shift == xsymbols.shift"
   16.19  
   16.20  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   16.21    by (simp add: shift_def)
   16.22 @@ -47,23 +51,27 @@
   16.23    typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   16.24    typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
   16.25  
   16.26 -abbreviation (output)
   16.27 +abbreviation
   16.28    funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
   16.29 -  "Ts =>> T = foldr Fun Ts T"
   16.30 +  "Ts =>> T == foldr Fun Ts T"
   16.31  
   16.32    typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
   16.33 -  "(env |- t : T) = ((env, t, T) \<in> typing)"
   16.34 +  "env |- t : T == (env, t, T) \<in> typing"
   16.35  
   16.36    typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
   16.37      ("_ ||- _ : _" [50, 50, 50] 50)
   16.38 -  "(env ||- ts : Ts) = typings env ts Ts"
   16.39 +  "env ||- ts : Ts == typings env ts Ts"
   16.40  
   16.41 -syntax (xsymbols)
   16.42 +abbreviation (xsymbols)
   16.43    typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   16.44 -syntax (latex)
   16.45 +  "env \<turnstile> t : T == env |- t : T"
   16.46 +
   16.47 +abbreviation (latex)
   16.48    funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
   16.49 +  "op \<Rrightarrow> == op =>>"
   16.50    typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
   16.51      ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
   16.52 +  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
   16.53  
   16.54  inductive typing
   16.55    intros
    17.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:12:02 2006 +0200
    17.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:51:06 2006 +0200
    17.3 @@ -361,11 +361,13 @@
    17.4  consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
    17.5    rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
    17.6  
    17.7 -abbreviation (output)
    17.8 +abbreviation
    17.9    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
   17.10 -  "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
   17.11 -syntax (xsymbols)
   17.12 +  "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
   17.13 +
   17.14 +abbreviation (xsymbols)
   17.15    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   17.16 +  "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
   17.17  
   17.18  inductive rtyping
   17.19    intros
    18.1 --- a/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:12:02 2006 +0200
    18.2 +++ b/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:51:06 2006 +0200
    18.3 @@ -23,7 +23,7 @@
    18.4    intros
    18.5      accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    18.6  
    18.7 -abbreviation (output)
    18.8 +abbreviation
    18.9    termi :: "('a \<times> 'a) set => 'a set"
   18.10    "termi r == acc (r\<inverse>)"
   18.11  
    19.1 --- a/src/HOL/Library/Multiset.thy	Sat Apr 08 22:12:02 2006 +0200
    19.2 +++ b/src/HOL/Library/Multiset.thy	Sat Apr 08 22:51:06 2006 +0200
    19.3 @@ -33,9 +33,9 @@
    19.4    MCollect :: "'a multiset => ('a => bool) => 'a multiset"
    19.5    "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
    19.6  
    19.7 -abbreviation (output)
    19.8 +abbreviation
    19.9    Melem :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
   19.10 -  "(a :# M) = (0 < count M a)"
   19.11 +  "a :# M == 0 < count M a"
   19.12  
   19.13  syntax
   19.14    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
    20.1 --- a/src/HOL/List.thy	Sat Apr 08 22:12:02 2006 +0200
    20.2 +++ b/src/HOL/List.thy	Sat Apr 08 22:51:06 2006 +0200
    20.3 @@ -54,9 +54,9 @@
    20.4    filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    20.5    map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"
    20.6  
    20.7 -abbreviation (output)
    20.8 - upto:: "nat => nat => nat list"    ("(1[_../_])")
    20.9 -"[i..j] = [i..<(Suc j)]"
   20.10 +abbreviation
   20.11 +  upto:: "nat => nat => nat list"    ("(1[_../_])")
   20.12 +  "[i..j] == [i..<(Suc j)]"
   20.13  
   20.14  
   20.15  nonterminals lupdbinds lupdbind
   20.16 @@ -93,9 +93,9 @@
   20.17    Function @{text size} is overloaded for all datatypes. Users may
   20.18    refer to the list version as @{text length}. *}
   20.19  
   20.20 -abbreviation (output)
   20.21 - length :: "'a list => nat"
   20.22 -"length = size"
   20.23 +abbreviation
   20.24 +  length :: "'a list => nat"
   20.25 +  "length == size"
   20.26  
   20.27  primrec
   20.28    "hd(x#xs) = x"
    21.1 --- a/src/HOL/Relation.thy	Sat Apr 08 22:12:02 2006 +0200
    21.2 +++ b/src/HOL/Relation.thy	Sat Apr 08 22:51:06 2006 +0200
    21.3 @@ -58,9 +58,9 @@
    21.4    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
    21.5    "inv_image r f == {(x, y). (f x, f y) : r}"
    21.6  
    21.7 -abbreviation (output)
    21.8 +abbreviation
    21.9    reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
   21.10 -  "reflexive = refl UNIV"
   21.11 +  "reflexive == refl UNIV"
   21.12  
   21.13  
   21.14  subsection {* The identity relation *}
    22.1 --- a/src/HOL/Set.thy	Sat Apr 08 22:12:02 2006 +0200
    22.2 +++ b/src/HOL/Set.thy	Sat Apr 08 22:51:06 2006 +0200
    22.3 @@ -47,9 +47,9 @@
    22.4  
    22.5  subsection {* Additional concrete syntax *}
    22.6  
    22.7 -abbreviation (output)
    22.8 +abbreviation
    22.9    range :: "('a => 'b) => 'b set"             -- "of function"
   22.10 -  "range f  =  f ` UNIV"
   22.11 +  "range f == f ` UNIV"
   22.12  
   22.13  syntax
   22.14    "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
    23.1 --- a/src/HOL/Unix/Unix.thy	Sat Apr 08 22:12:02 2006 +0200
    23.2 +++ b/src/HOL/Unix/Unix.thy	Sat Apr 08 22:51:06 2006 +0200
    23.3 @@ -352,11 +352,9 @@
    23.4  consts
    23.5    transition :: "(file \<times> operation \<times> file) set"
    23.6  
    23.7 -syntax
    23.8 -  "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    23.9 -  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
   23.10 -translations
   23.11 -  "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition"
   23.12 +abbreviation
   23.13 +  transition_rel  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
   23.14 +  "root \<midarrow>x\<rightarrow> root' \<equiv> (root, x, root') \<in> transition"
   23.15  
   23.16  inductive transition
   23.17    intros
   23.18 @@ -510,11 +508,9 @@
   23.19  consts
   23.20    transitions :: "(file \<times> operation list \<times> file) set"
   23.21  
   23.22 -syntax
   23.23 -  "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
   23.24 -  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
   23.25 -translations
   23.26 -  "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions"
   23.27 +abbreviation
   23.28 +  transitions_rel  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
   23.29 +  "root =xs\<Rightarrow> root' \<equiv> (root, xs, root') \<in> transitions"
   23.30  
   23.31  inductive transitions
   23.32    intros
    24.1 --- a/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:12:02 2006 +0200
    24.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:51:06 2006 +0200
    24.3 @@ -37,8 +37,8 @@
    24.4      Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
    24.5        (succ m, r m n) \<in> REC zero succ e r"
    24.6  
    24.7 -abbreviation (in NAT) (output)
    24.8 -  "Rec = REC zero succ"
    24.9 +abbreviation (in NAT)
   24.10 +  "Rec == REC zero succ"
   24.11  
   24.12  lemma (in NAT) Rec_functional:
   24.13    fixes x :: 'n
    25.1 --- a/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:12:02 2006 +0200
    25.2 +++ b/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:51:06 2006 +0200
    25.3 @@ -150,7 +150,7 @@
    25.4  
    25.5  abbreviation (in monoid)
    25.6    abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
    25.7 -    "(x \<^loc>\<up> n) = npow n x"
    25.8 +  "x \<^loc>\<up> n == npow n x"
    25.9  
   25.10  lemma (in monoid) npow_def:
   25.11    "x \<^loc>\<up> 0 = \<^loc>\<one>"
   25.12 @@ -290,7 +290,7 @@
   25.13  
   25.14  abbreviation (in group)
   25.15    abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
   25.16 -    "(x \<^loc>\<up> k) = pow k x"
   25.17 +  "x \<^loc>\<up> k == pow k x"
   25.18  
   25.19  lemma (in group) int_pow_zero:
   25.20    "x \<^loc>\<up> (0::int) = \<^loc>\<one>"