# HG changeset patch
# User wenzelm
# Date 1144529466 -7200
# Node ID 667b5ea637dd36dd23dbc3093ef44ba1ea7dc640
# Parent  638bbd5a4a3bd34199cffec545ee4e12e5d26b08
refined 'abbreviation';

diff -r 638bbd5a4a3b -r 667b5ea637dd NEWS
--- a/NEWS	Sat Apr 08 22:12:02 2006 +0200
+++ b/NEWS	Sat Apr 08 22:51:06 2006 +0200
@@ -144,9 +144,9 @@
     eq  (infix "===" 50)
     where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
 
-  abbreviation (output)
+  abbreviation
     neq  (infix "=!=" 50)
-    "(x =!= y) <-> ~ (x === y)"
+    "x =!= y == ~ (x === y)"
 
 These specifications may be also used in a locale context.  Then the
 constants being introduced depend on certain fixed parameters, and the
@@ -157,10 +157,9 @@
 entities from a monomorphic theory.
 
 Presently, abbreviations are only available 'in' a target locale, but
-not inherited by general import expressions.
-
-Also note that 'abbreviation' may be used as a type-safe replacement
-for 'syntax' + 'translations' in common applications.
+not inherited by general import expressions.  Also note that
+'abbreviation' may be used as a type-safe replacement for 'syntax' +
+'translations' in common applications.
 
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level
diff -r 638bbd5a4a3b -r 667b5ea637dd doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Apr 08 22:12:02 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Apr 08 22:51:06 2006 +0200
@@ -24,7 +24,7 @@
   'definition' locale? (constdecl? constdef +)
   ;
 
-  'abbreviation' locale? '(output)'? (constdecl? prop +)
+  'abbreviation' locale? mode? (constdecl? prop +)
   ;
   'axiomatization' locale? consts? ('where' specs)?
   ;
@@ -55,16 +55,20 @@
   supported here.
   
 \item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
-  a syntactic constant which is associated with a certain term derived
-  from the specification given as $eq$.  The very same transformations
-  as for $\isarkeyword{definition}$ are applied here, although
-  additional conditions are not supported.
+  a syntactic constant which is associated with a certain term
+  according to the meta-level equality $eq$.
   
   Abbreviations participate in the usual type-inference process, but
-  are expanded before the logic ever sees them.  The expansion is
-  one-way by default; the ``$(output)$'' option makes abbreviations
-  fold back whenever terms are pretty printed.  The latter needs some
-  care to avoid overlapping or looping syntactic replacements!
+  are expanded before the logic ever sees them.  Pretty printing of
+  terms involves higher-order rewriting with rules stemming from
+  reverted abbreviations.  This needs some care to avoid overlapping
+  or looping syntactic replacements!
+  
+  The optional $mode$ specification restricts output to a particular
+  print mode; using ``$input$'' here achieves the effect of one-way
+  abbreviations.  The mode may also include an ``$output$'' qualifier
+  that affects the concrete syntax declared for abbreviations, cf.\ 
+  $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
   
 \item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
   \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
diff -r 638bbd5a4a3b -r 667b5ea637dd src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/FOL/IFOL.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -45,10 +45,18 @@
   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
 
 
-abbreviation (output)
+abbreviation
   not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
   "x ~= y == ~ (x = y)"
 
+abbreviation (xsymbols)
+  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
+  "x \<noteq> y == ~ (x = y)"
+
+abbreviation (HTML output)
+  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
+  "not_equal == xsymbols.not_equal"
+
 syntax (xsymbols)
   Not           :: "o => o"                     ("\<not> _" [40] 40)
   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
@@ -56,7 +64,6 @@
   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
 
@@ -67,7 +74,6 @@
   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
 
 
 local
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Auth/Guard/Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -19,9 +19,9 @@
 
 subsubsection{*a little abbreviation*}
 
-syntax Ciph :: "agent => msg"
-
-translations "Ciph A X" == "Crypt (shrK A) X"
+abbreviation
+  Ciph :: "agent => msg => msg"
+  "Ciph A X == Crypt (shrK A) X"
 
 subsubsection{*agent associated to a key*}
 
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -163,9 +163,9 @@
   fixes r and f
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
-abbreviation (output)
+abbreviation
   RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
-  "f respects r = congruent r f"
+  "f respects r == congruent r f"
 
 
 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -13,8 +13,8 @@
 subsection {* Definition and basic properties *}
 
 consts Finites :: "'a set set"
-abbreviation (output)
-  "finite A = (A : Finites)"
+abbreviation
+  "finite A == A : Finites"
 
 inductive Finites
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Fun.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -59,19 +59,19 @@
 
 constdefs
   inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
-    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
 
 text{*A common special case: functions injective over the entire domain type.*}
 
-abbreviation (output)
-  "inj f = inj_on f UNIV"
+abbreviation
+  "inj f == inj_on f UNIV"
 
 constdefs
   surj :: "('a => 'b) => bool"                   (*surjective*)
-    "surj f == ! y. ? x. y=f(x)"
+  "surj f == ! y. ? x. y=f(x)"
 
   bij :: "('a => 'b) => bool"                    (*bijective*)
-    "bij f == inj f & surj f"
+  "bij f == inj f & surj f"
 
 
 
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Infinite_Set.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -13,12 +13,9 @@
 
 text {* Some elementary facts about infinite sets, by Stefan Merz. *}
 
-syntax infinite :: "'a set \<Rightarrow> bool"
-translations "infinite S" == "\<not> finite S"
-(* doesnt work:
-abbreviation (output)
-  "infinite S = (\<not> finite S)"
-*)
+abbreviation
+  infinite :: "'a set \<Rightarrow> bool"
+  "infinite S == \<not> finite S"
 
 text {*
   Infinite sets are non-empty, and if we remove some elements
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -31,7 +31,7 @@
   | Cond "'a bexp" "'a com" "'a com"
   | While "'a bexp" "'a assn" "'a com"
 
-abbreviation (output)
+abbreviation
   Skip  ("SKIP")
   "SKIP == Basic id"
 
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -25,9 +25,9 @@
   "Church_Rosser R =
     (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
 
-abbreviation (output)
+abbreviation
   confluent :: "('a \<times> 'a) set => bool"
-  "confluent R = diamond (R^*)"
+  "confluent R == diamond (R^*)"
 
 
 subsection {* Basic lemmas *}
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -21,13 +21,13 @@
 consts
   eta :: "(dB \<times> dB) set"
 
-abbreviation (output)
+abbreviation
   eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
-  "(s -e> t) = ((s, t) \<in> eta)"
+  "s -e> t == (s, t) \<in> eta"
   eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
-  "(s -e>> t) = ((s, t) \<in> eta^*)"
+  "s -e>> t == (s, t) \<in> eta^*"
   eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
-  "(s -e>= t) = ((s, t) \<in> eta^=)"
+  "s -e>= t == (s, t) \<in> eta^="
 
 inductive eta
   intros
@@ -224,12 +224,13 @@
 consts
   par_eta :: "(dB \<times> dB) set"
 
-abbreviation (output)
+abbreviation
   par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
-  "(s =e> t) = ((s, t) \<in> par_eta)"
+  "s =e> t == (s, t) \<in> par_eta"
 
-syntax (xsymbols)
+abbreviation (xsymbols)
   par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
+  "op \<Rightarrow>\<^sub>\<eta> == op =e>"
 
 inductive par_eta
 intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -56,15 +56,17 @@
 consts
   beta :: "(dB \<times> dB) set"
 
-abbreviation (output)
+abbreviation
   beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
-  "(s -> t) = ((s, t) \<in> beta)"
+  "s -> t == (s, t) \<in> beta"
   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
-  "(s ->> t) = ((s, t) \<in> beta^*)"
+  "s ->> t == (s, t) \<in> beta^*"
 
-syntax (latex)
+abbreviation (latex)
   beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  "op \<rightarrow>\<^sub>\<beta> == op ->"
   beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
+  "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
 
 inductive beta
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -8,9 +8,9 @@
 
 theory ListApplication imports Lambda begin
 
-abbreviation (output)
+abbreviation
   list_application :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
-  "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
+  "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
 
 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
   by (induct ts rule: rev_induct) auto
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -12,9 +12,9 @@
   Lifting beta-reduction to lists of terms, reducing exactly one element.
 *}
 
-abbreviation (output)
+abbreviation
   list_beta :: "dB list => dB list => bool"   (infixl "=>" 50)
-  "(rs => ss) = ((rs, ss) : step1 beta)"
+  "rs => ss == (rs, ss) : step1 beta"
 
 lemma head_Var_reduction:
   "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -17,9 +17,9 @@
 consts
   par_beta :: "(dB \<times> dB) set"
 
-abbreviation (output)
+abbreviation
   par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
-  "(s => t) = ((s, t) \<in> par_beta)"
+  "s => t == (s, t) \<in> par_beta"
 
 inductive par_beta
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Type.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -14,10 +14,14 @@
 definition
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
   "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-syntax (xsymbols)
-  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-syntax (HTML output)
-  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+
+abbreviation (xsymbols)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  "e\<langle>i:a\<rangle> == e<i:a>"
+
+abbreviation (HTML output)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  "shift == xsymbols.shift"
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
@@ -47,23 +51,27 @@
   typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
 
-abbreviation (output)
+abbreviation
   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
-  "Ts =>> T = foldr Fun Ts T"
+  "Ts =>> T == foldr Fun Ts T"
 
   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
-  "(env |- t : T) = ((env, t, T) \<in> typing)"
+  "env |- t : T == (env, t, T) \<in> typing"
 
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ ||- _ : _" [50, 50, 50] 50)
-  "(env ||- ts : Ts) = typings env ts Ts"
+  "env ||- ts : Ts == typings env ts Ts"
 
-syntax (xsymbols)
+abbreviation (xsymbols)
   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-syntax (latex)
+  "env \<turnstile> t : T == env |- t : T"
+
+abbreviation (latex)
   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
+  "op \<Rrightarrow> == op =>>"
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
+  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
 
 inductive typing
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -361,11 +361,13 @@
 consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
   rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
 
-abbreviation (output)
+abbreviation
   rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
-  "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
-syntax (xsymbols)
+  "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
+
+abbreviation (xsymbols)
   rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+  "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
 
 inductive rtyping
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -23,7 +23,7 @@
   intros
     accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
 
-abbreviation (output)
+abbreviation
   termi :: "('a \<times> 'a) set => 'a set"
   "termi r == acc (r\<inverse>)"
 
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -33,9 +33,9 @@
   MCollect :: "'a multiset => ('a => bool) => 'a multiset"
   "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
 
-abbreviation (output)
+abbreviation
   Melem :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
-  "(a :# M) = (0 < count M a)"
+  "a :# M == 0 < count M a"
 
 syntax
   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/List.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -54,9 +54,9 @@
   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"
 
-abbreviation (output)
- upto:: "nat => nat => nat list"    ("(1[_../_])")
-"[i..j] = [i..<(Suc j)]"
+abbreviation
+  upto:: "nat => nat => nat list"    ("(1[_../_])")
+  "[i..j] == [i..<(Suc j)]"
 
 
 nonterminals lupdbinds lupdbind
@@ -93,9 +93,9 @@
   Function @{text size} is overloaded for all datatypes. Users may
   refer to the list version as @{text length}. *}
 
-abbreviation (output)
- length :: "'a list => nat"
-"length = size"
+abbreviation
+  length :: "'a list => nat"
+  "length == size"
 
 primrec
   "hd(x#xs) = x"
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Relation.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -58,9 +58,9 @@
   inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
   "inv_image r f == {(x, y). (f x, f y) : r}"
 
-abbreviation (output)
+abbreviation
   reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
-  "reflexive = refl UNIV"
+  "reflexive == refl UNIV"
 
 
 subsection {* The identity relation *}
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Set.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -47,9 +47,9 @@
 
 subsection {* Additional concrete syntax *}
 
-abbreviation (output)
+abbreviation
   range :: "('a => 'b) => 'b set"             -- "of function"
-  "range f  =  f ` UNIV"
+  "range f == f ` UNIV"
 
 syntax
   "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Unix/Unix.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -352,11 +352,9 @@
 consts
   transition :: "(file \<times> operation \<times> file) set"
 
-syntax
-  "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
-  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
-translations
-  "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition"
+abbreviation
+  transition_rel  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
+  "root \<midarrow>x\<rightarrow> root' \<equiv> (root, x, root') \<in> transition"
 
 inductive transition
   intros
@@ -510,11 +508,9 @@
 consts
   transitions :: "(file \<times> operation list \<times> file) set"
 
-syntax
-  "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
-  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
-translations
-  "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions"
+abbreviation
+  transitions_rel  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
+  "root =xs\<Rightarrow> root' \<equiv> (root, xs, root') \<in> transitions"
 
 inductive transitions
   intros
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -37,8 +37,8 @@
     Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
       (succ m, r m n) \<in> REC zero succ e r"
 
-abbreviation (in NAT) (output)
-  "Rec = REC zero succ"
+abbreviation (in NAT)
+  "Rec == REC zero succ"
 
 lemma (in NAT) Rec_functional:
   fixes x :: 'n
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -150,7 +150,7 @@
 
 abbreviation (in monoid)
   abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
-    "(x \<^loc>\<up> n) = npow n x"
+  "x \<^loc>\<up> n == npow n x"
 
 lemma (in monoid) npow_def:
   "x \<^loc>\<up> 0 = \<^loc>\<one>"
@@ -290,7 +290,7 @@
 
 abbreviation (in group)
   abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
-    "(x \<^loc>\<up> k) = pow k x"
+  "x \<^loc>\<up> k == pow k x"
 
 lemma (in group) int_pow_zero:
   "x \<^loc>\<up> (0::int) = \<^loc>\<one>"