# HG changeset patch
# User wenzelm
# Date 1147807981 -7200
# Node ID 09be06943252a2b2d1f5b1775cb6fff29aa7ec7a
# Parent  f10b141078e7e1fc41a79809f0567f75e8598446
tuned concrete syntax -- abbreviation/const_syntax;

diff -r f10b141078e7 -r 09be06943252 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/FOL/IFOL.thy	Tue May 16 21:33:01 2006 +0200
@@ -49,13 +49,11 @@
   not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
   "x ~= y == ~ (x = y)"
 
-abbreviation (xsymbols)
-  not_equal1  (infixl "\<noteq>" 50)
-  "x \<noteq> y == ~ (x = y)"
+const_syntax (xsymbols)
+  not_equal  (infixl "\<noteq>" 50)
 
-abbreviation (HTML output)
-  not_equal2  (infixl "\<noteq>" 50)
-  "not_equal2 == not_equal"
+const_syntax (HTML output)
+  not_equal  (infixl "\<noteq>" 50)
 
 syntax (xsymbols)
   Not           :: "o => o"                     ("\<not> _" [40] 40)
diff -r f10b141078e7 -r 09be06943252 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Fun.thy	Tue May 16 21:33:01 2006 +0200
@@ -48,17 +48,15 @@
   comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
   "f o g == %x. f(g(x))"
 
+const_syntax (xsymbols)
+  comp  (infixl "\<circ>" 55)
+
+const_syntax (HTML output)
+  comp  (infixl "\<circ>" 55)
+
 text{*compatibility*}
 lemmas o_def = comp_def
 
-abbreviation (xsymbols)
-  comp1  (infixl "\<circ>" 55)
-  "comp1 == comp"
-
-abbreviation (HTML output)
-  comp2  (infixl "\<circ>" 55)
-  "comp2 == comp"
-
 constdefs
   inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
   "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
diff -r f10b141078e7 -r 09be06943252 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/HOL.thy	Tue May 16 21:33:01 2006 +0200
@@ -52,14 +52,45 @@
 consts
   If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
 
+
 subsubsection {* Additional concrete syntax *}
 
+const_syntax (output)
+  "op ="  (infix "=" 50)
+
+abbreviation
+  not_equal     :: "['a, 'a] => bool"               (infixl "~=" 50)
+  "x ~= y == ~ (x = y)"
+
+const_syntax (output)
+  not_equal  (infix "~=" 50)
+
+const_syntax (xsymbols)
+  Not  ("\<not> _" [40] 40)
+  "op &"  (infixr "\<and>" 35)
+  "op |"  (infixr "\<or>" 30)
+  "op -->"  (infixr "\<longrightarrow>" 25)
+  not_equal  (infix "\<noteq>" 50)
+
+const_syntax (HTML output)
+  Not  ("\<not> _" [40] 40)
+  "op &"  (infixr "\<and>" 35)
+  "op |"  (infixr "\<or>" 30)
+  not_equal  (infix "\<noteq>" 50)
+
+abbreviation (iff)
+  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
+  "A <-> B == A = B"
+
+const_syntax (xsymbols)
+  iff  (infixr "\<longleftrightarrow>" 25)
+
+
 nonterminals
   letbinds  letbind
   case_syn  cases_syn
 
 syntax
-  "_not_equal"  :: "['a, 'a] => bool"                    (infixl "~=" 50)
   "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
 
   "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
@@ -73,7 +104,6 @@
   "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
 
 translations
-  "x ~= y"                == "~ (x = y)"
   "THE x. P"              == "The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
@@ -85,31 +115,14 @@
      in Syntax.const "_The" $ x $ t end)]
 *}
 
-syntax (output)
-  "="           :: "['a, 'a] => bool"                    (infix 50)
-  "_not_equal"  :: "['a, 'a] => bool"                    (infix "~=" 50)
-
 syntax (xsymbols)
-  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
-  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
-  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
-  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
-  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
   "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
 (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
 
-syntax (xsymbols output)
-  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
-
 syntax (HTML output)
-  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
-  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
-  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
-  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
-  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
   "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
@@ -119,14 +132,6 @@
   "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
 
-abbreviation (iff)
-  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
-  "A <-> B == A = B"
-
-abbreviation (xsymbols)
-  iff1  (infixr "\<longleftrightarrow>" 25)
-  "A \<longleftrightarrow> B == A <-> B"
-
 
 subsubsection {* Axioms and basic definitions *}
 
@@ -181,6 +186,7 @@
   The
   arbitrary
 
+
 subsubsection {* Generic algebraic operations *}
 
 axclass zero < type
diff -r f10b141078e7 -r 09be06943252 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Infinite_Set.thy	Tue May 16 21:33:01 2006 +0200
@@ -346,29 +346,24 @@
   so we introduce corresponding binders and their proof rules.
 *}
 
-consts
+definition
   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
+  INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
   Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
-
-defs
-  INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
 
-abbreviation (xsymbols)
-  Inf_many1  (binder "\<exists>\<^sub>\<infinity>" 10)
-  "Inf_many1 == Inf_many"
-  Alm_all1  (binder "\<forall>\<^sub>\<infinity>" 10)
-  "Alm_all1 == Alm_all"
+const_syntax (xsymbols)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
 
-abbreviation (HTML output)
-  Inf_many2  (binder "\<exists>\<^sub>\<infinity>" 10)
-  "Inf_many2 == Inf_many"
-  Alm_all2  (binder "\<forall>\<^sub>\<infinity>" 10)
-  "Alm_all2 == Alm_all"
+const_syntax (HTML output)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
 
 lemma INF_EX:
   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
-proof (unfold INF_def, rule ccontr)
+  unfolding INF_def
+proof (rule ccontr)
   assume inf: "infinite {x. P x}"
     and notP: "\<not>(\<exists>x. P x)"
   from notP have "{x. P x} = {}" by simp
@@ -418,7 +413,7 @@
   These simplify the reasoning about deterministic automata.
 *}
 
-constdefs
+definition
   atmost_one :: "'a set \<Rightarrow> bool"
   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
 
diff -r f10b141078e7 -r 09be06943252 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue May 16 21:33:01 2006 +0200
@@ -567,9 +567,8 @@
   Nats  :: "'a::comm_semiring_1_cancel set"
   "Nats == range of_nat"
 
-abbreviation (xsymbols)
-  Nats1  ("\<nat>")
-  "\<nat> == Nats"
+const_syntax (xsymbols)
+  Nats  ("\<nat>")
 
 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
 by (simp add: Nats_def)
@@ -701,9 +700,8 @@
   Ints  :: "'a::comm_ring_1 set"
   "Ints == range of_int"
 
-abbreviation (xsymbols)
-  Ints1  ("\<int>")
-  "\<int> == Ints"
+const_syntax (xsymbols)
+  Ints  ("\<int>")
 
 lemma Ints_0 [simp]: "0 \<in> Ints"
 apply (simp add: Ints_def)
diff -r f10b141078e7 -r 09be06943252 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue May 16 21:33:01 2006 +0200
@@ -24,13 +24,11 @@
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
   "x\<twosuperior> == x^2"
 
-abbreviation (latex output)
-  square1  ("(_\<twosuperior>)" [1000] 999)
-  "square1 x == x^2"
+const_syntax (latex output)
+  square  ("(_\<twosuperior>)" [1000] 999)
 
-abbreviation (HTML output)
-  square2  ("(_\<twosuperior>)" [1000] 999)
-  "square2 x == x^2"
+const_syntax (HTML output)
+  square  ("(_\<twosuperior>)" [1000] 999)
 
 
 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
diff -r f10b141078e7 -r 09be06943252 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy	Tue May 16 21:33:01 2006 +0200
@@ -228,9 +228,8 @@
   par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
   "s =e> t == (s, t) \<in> par_eta"
 
-abbreviation (xsymbols)
-  par_eta_red1 :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
-  "op \<Rightarrow>\<^sub>\<eta> == op =e>"
+const_syntax (xsymbols)
+  par_eta_red  (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
 
 inductive par_eta
 intros
@@ -300,7 +299,8 @@
   assumes u: "u => u'"
   shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
 proof (induct k fixing: t t')
-  case 0 with u show ?case by simp
+  case 0
+  with u show ?case by simp
 next
   case (Suc k)
   hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]"
@@ -387,7 +387,7 @@
 subsection {* Eta-postponement theorem *}
 
 text {*
-Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
+  Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
 *}
 
 theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
@@ -428,7 +428,7 @@
       and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
       by (blast dest: par_eta_elim_app par_eta_elim_abs)
     from beta have "size q' < size t" and "size r' < size t" by simp_all
-    with beta(2,3) qq rr obtain t' t'' where "q => t'" and
+    with beta(2-3) qq rr obtain t' t'' where "q => t'" and
       "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
       by (blast dest: less(1))
     with s beta show ?thesis
diff -r f10b141078e7 -r 09be06943252 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Tue May 16 21:33:01 2006 +0200
@@ -62,11 +62,9 @@
   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
   "s ->> t == (s, t) \<in> beta^*"
 
-abbreviation (latex)
-  beta_red1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
-  "op \<rightarrow>\<^sub>\<beta> == op ->"
-  beta_reds1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
-  "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
+const_syntax (latex)
+  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
 inductive beta
   intros
@@ -100,9 +98,7 @@
 
 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
-  apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
-    intro: rtrancl_trans)
-  done
+  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
 
 
 subsection {* Substitution-lemmas *}
diff -r f10b141078e7 -r 09be06943252 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Type.thy	Tue May 16 21:33:01 2006 +0200
@@ -15,13 +15,11 @@
   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))"
 
-abbreviation (xsymbols)
-  shift1  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-  "e\<langle>i:a\<rangle> == e<i:a>"
+const_syntax (xsymbols)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 
-abbreviation (HTML output)
-  shift2  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-  "shift2 == shift"
+const_syntax (HTML output)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
@@ -62,16 +60,12 @@
     ("_ ||- _ : _" [50, 50, 50] 50)
   "env ||- ts : Ts == typings env ts Ts"
 
-abbreviation (xsymbols)
-  typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-  "env \<turnstile> t : T == env |- t : T"
+const_syntax (xsymbols)
+  typing_rel  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
 
-abbreviation (latex)
-  funs2 :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
-  "op \<Rrightarrow> == op =>>"
-  typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
-    ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
-  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
+const_syntax (latex)
+  funs  (infixr "\<Rrightarrow>" 200)
+  typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
 
 inductive typing
   intros
diff -r f10b141078e7 -r 09be06943252 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue May 16 21:33:01 2006 +0200
@@ -365,9 +365,8 @@
   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"
 
-abbreviation (xsymbols)
-  rtyping_rel1 :: "(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"
+const_syntax (xsymbols)
+  rtyping_rel  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
 
 inductive rtyping
   intros
diff -r f10b141078e7 -r 09be06943252 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue May 16 21:33:01 2006 +0200
@@ -23,9 +23,8 @@
   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
   "A -> B == Pi A (%_. B)"
 
-abbreviation (xsymbols)
-  funcset1  (infixr "\<rightarrow>" 60)
-  "funcset1 == funcset"
+const_syntax (xsymbols)
+  funcset  (infixr "\<rightarrow>" 60)
 
 syntax
   "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
diff -r f10b141078e7 -r 09be06943252 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy	Tue May 16 21:33:01 2006 +0200
@@ -58,7 +58,7 @@
   elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
   "a *o B == {c. EX b:B. c = a * b}"
 
-abbreviation (inout)
+abbreviation (input)
   elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
   "x =o A == x : A"
 
diff -r f10b141078e7 -r 09be06943252 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Map.thy	Tue May 16 21:33:01 2006 +0200
@@ -15,14 +15,20 @@
 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
 translations (type) "a ~=> b " <= (type) "a => b option"
 
+syntax (xsymbols)
+  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
+
 abbreviation
   empty     ::  "'a ~=> 'b"
   "empty == %x. None"
 
-constdefs
+definition
   map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
   "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
 
+const_syntax (xsymbols)
+  map_comp  (infixl "\<circ>\<^sub>m" 55)
+
 consts
 map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
 restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
@@ -32,6 +38,9 @@
 map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
 
+const_syntax (latex output)
+  restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
+
 nonterminals
   maplets maplet
 
@@ -44,17 +53,9 @@
   "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
 
 syntax (xsymbols)
-  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
-
-  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
-
   "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
   "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
 
-syntax (latex output)
-  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
-  --"requires amssymb!"
-
 translations
   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
   "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
diff -r f10b141078e7 -r 09be06943252 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Orderings.thy	Tue May 16 21:33:01 2006 +0200
@@ -17,21 +17,23 @@
 axclass
   ord < type
 
-syntax
-  "less"        :: "['a::ord, 'a] => bool"             ("op <")
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("op <=")
-
 consts
-  "less"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
+  less  :: "['a::ord, 'a] => bool"
+  less_eq  :: "['a::ord, 'a] => bool"
 
-syntax (xsymbols)
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
+const_syntax
+  less  ("op <")
+  less  ("(_/ < _)"  [50, 51] 50)
+  less_eq  ("op <=")
+  less_eq  ("(_/ <= _)" [50, 51] 50)
 
-syntax (HTML output)
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
-  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
+const_syntax (xsymbols)
+  less_eq  ("op \<le>")
+  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
+
+const_syntax (HTML output)
+  less_eq  ("op \<le>")
+  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
 
 abbreviation (input)
   greater  (infixl ">" 50)
@@ -39,13 +41,8 @@
   greater_eq  (infixl ">=" 50)
   "x >= y == y <= x"
 
-abbreviation (xsymbols)
-  greater_eq1  (infixl "\<ge>" 50)
-  "x \<ge> y == x >= y"
-
-abbreviation (HTML output)
-  greater_eq2  (infixl "\<ge>" 50)
-  "greater_eq2 == greater_eq"
+const_syntax (xsymbols)
+  greater_eq  (infixl "\<ge>" 50)
 
 
 subsection {* Monotonicity *}
diff -r f10b141078e7 -r 09be06943252 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Product_Type.thy	Tue May 16 21:33:01 2006 +0200
@@ -113,13 +113,11 @@
   Times :: "['a set, 'b set] => ('a * 'b) set"  (infixr "<*>" 80)
   "A <*> B == Sigma A (%_. B)"
 
-abbreviation (xsymbols)
-  Times1  (infixr "\<times>" 80)
-  "Times1 == Times"
+const_syntax (xsymbols)
+  Times  (infixr "\<times>" 80)
 
-abbreviation (HTML output)
-  Times2  (infixr "\<times>" 80)
-  "Times2 == Times"
+const_syntax (HTML output)
+  Times  (infixr "\<times>" 80)
 
 
 subsubsection {* Concrete syntax *}
diff -r f10b141078e7 -r 09be06943252 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Relation.thy	Tue May 16 21:33:01 2006 +0200
@@ -12,13 +12,14 @@
 
 subsection {* Definitions *}
 
-constdefs
+definition
   converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
   "r^-1 == {(y, x). (x, y) : r}"
-syntax (xsymbols)
-  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\<inverse>)" [1000] 999)
 
-constdefs
+const_syntax (xsymbols)
+  converse  ("(_\<inverse>)" [1000] 999)
+
+definition
   rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
   "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
 
diff -r f10b141078e7 -r 09be06943252 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Set.thy	Tue May 16 21:33:01 2006 +0200
@@ -34,11 +34,11 @@
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
   image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
-
-syntax
-  "op :"        :: "'a => 'a set => bool"                ("op :")
-consts
-  "op :"        :: "'a => 'a set => bool"                ("(_/ : _)" [50, 51] 50)  -- "membership"
+  "op :"        :: "'a => 'a set => bool"                -- "membership"
+
+const_syntax
+  "op :"  ("op :")
+  "op :"  ("(_/ : _)" [50, 51] 50)
 
 local
 
@@ -51,10 +51,62 @@
   range :: "('a => 'b) => 'b set"             -- "of function"
   "range f == f ` UNIV"
 
+abbreviation
+  "not_mem x A == ~ (x : A)"                  -- "non-membership"
+
+const_syntax
+  not_mem  ("op ~:")
+  not_mem  ("(_/ ~: _)" [50, 51] 50)
+
+const_syntax (xsymbols)
+  "op Int"  (infixl "\<inter>" 70)
+  "op Un"  (infixl "\<union>" 65)
+  "op :"  ("op \<in>")
+  "op :"  ("(_/ \<in> _)" [50, 51] 50)
+  not_mem  ("op \<notin>")
+  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
+  Union  ("\<Union>_" [90] 90)
+  Inter  ("\<Inter>_" [90] 90)
+
+const_syntax (HTML output)
+  "op Int"  (infixl "\<inter>" 70)
+  "op Un"  (infixl "\<union>" 65)
+  "op :"  ("op \<in>")
+  "op :"  ("(_/ \<in> _)" [50, 51] 50)
+  not_mem  ("op \<notin>")
+  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
+
+abbreviation
+  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  "subset == less"
+  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  "subset_eq == less_eq"
+
+const_syntax (output)
+  subset  ("op <")
+  subset  ("(_/ < _)" [50, 51] 50)
+  subset_eq  ("op <=")
+  subset_eq  ("(_/ <= _)" [50, 51] 50)
+
+const_syntax (xsymbols)
+  subset  ("op \<subset>")
+  subset  ("(_/ \<subset> _)" [50, 51] 50)
+  subset_eq  ("op \<subseteq>")
+  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+
+const_syntax (HTML output)
+  subset  ("op \<subset>")
+  subset  ("(_/ \<subset> _)" [50, 51] 50)
+  subset_eq  ("op \<subseteq>")
+  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+
+abbreviation (input)
+  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infixl "\<supset>" 50)
+  "supset == greater"
+  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "\<supseteq>" 50)
+  "supset_eq == greater_eq"
+
 syntax
-  "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
-  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
-
   "@Finset"     :: "args => 'a set"                       ("{(_)}")
   "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
   "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
@@ -63,18 +115,15 @@
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
-
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   "_Bleast"       :: "id => 'a set => bool => 'a"      ("(3LEAST _:_./ _)" [0, 0, 10] 10)
 
-
 syntax (HOL)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
 
 translations
-  "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
   "{x. P}"      == "Collect (%x. P)"
@@ -91,41 +140,12 @@
   "EX x:A. P"   == "Bex A (%x. P)"
   "LEAST x:A. P" => "LEAST x. x:A & P"
 
-
-syntax (output)
-  "_setle"      :: "'a set => 'a set => bool"             ("op <=")
-  "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
-  "_setless"    :: "'a set => 'a set => bool"             ("op <")
-  "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
-
 syntax (xsymbols)
-  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
-  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
-  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
-  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
-  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
-  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
-  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
-  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
-  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
-  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
-  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
-  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
 
 syntax (HTML output)
-  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
-  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
-  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
-  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
-  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
-  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
-  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
-  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
-  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
-  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
 
@@ -135,47 +155,25 @@
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
-(*
-syntax (xsymbols)
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
-*)
+
 syntax (latex output)
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
 
-text{* Note the difference between ordinary xsymbol syntax of indexed
-unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
-and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
-former does not make the index expression a subscript of the
-union/intersection symbol because this leads to problems with nested
-subscripts in Proof General.  *}
-
-
-translations
-  "op \<subseteq>" => "op <= :: _ set => _ set => bool"
-  "op \<subset>" => "op <  :: _ set => _ set => bool"
-
-typed_print_translation {*
-  let
-    fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
-          list_comb (Syntax.const "_setle", ts)
-      | le_tr' _ _ _ = raise Match;
-
-    fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
-          list_comb (Syntax.const "_setless", ts)
-      | less_tr' _ _ _ = raise Match;
-  in [("less_eq", le_tr'), ("less", less_tr')] end
-*}
+text{*
+  Note the difference between ordinary xsymbol syntax of indexed
+  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
+  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
+  former does not make the index expression a subscript of the
+  union/intersection symbol because this leads to problems with nested
+  subscripts in Proof General. *}
 
 
 subsubsection "Bounded quantifiers"
 
-syntax
+syntax (output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
@@ -187,7 +185,7 @@
   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
 
-syntax (HOL)
+syntax (HOL output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
diff -r f10b141078e7 -r 09be06943252 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue May 16 21:33:01 2006 +0200
@@ -36,20 +36,19 @@
     r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
     trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
 
-syntax
-  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
-translations
-  "r^=" == "r \<union> Id"
+abbreviation
+  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
+  "r^= == r \<union> Id"
 
-syntax (xsymbols)
-  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
-  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
-  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
+const_syntax (xsymbols)
+  rtrancl  ("(_\<^sup>*)" [1000] 999)
+  trancl  ("(_\<^sup>+)" [1000] 999)
+  reflcl  ("(_\<^sup>=)" [1000] 999)
 
-syntax (HTML output)
-  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
-  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
-  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
+const_syntax (HTML output)
+  rtrancl  ("(_\<^sup>*)" [1000] 999)
+  trancl  ("(_\<^sup>+)" [1000] 999)
+  reflcl  ("(_\<^sup>=)" [1000] 999)
 
 
 subsection {* Reflexive-transitive closure *}