tuned concrete syntax -- abbreviation/const_syntax;
authorwenzelm
Tue May 16 21:33:01 2006 +0200 (2006-05-16)
changeset 1965609be06943252
parent 19655 f10b141078e7
child 19657 25eaa3660123
tuned concrete syntax -- abbreviation/const_syntax;
src/FOL/IFOL.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Infinite_Set.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Map.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/FOL/IFOL.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -49,13 +49,11 @@
     1.4    not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
     1.5    "x ~= y == ~ (x = y)"
     1.6  
     1.7 -abbreviation (xsymbols)
     1.8 -  not_equal1  (infixl "\<noteq>" 50)
     1.9 -  "x \<noteq> y == ~ (x = y)"
    1.10 +const_syntax (xsymbols)
    1.11 +  not_equal  (infixl "\<noteq>" 50)
    1.12  
    1.13 -abbreviation (HTML output)
    1.14 -  not_equal2  (infixl "\<noteq>" 50)
    1.15 -  "not_equal2 == not_equal"
    1.16 +const_syntax (HTML output)
    1.17 +  not_equal  (infixl "\<noteq>" 50)
    1.18  
    1.19  syntax (xsymbols)
    1.20    Not           :: "o => o"                     ("\<not> _" [40] 40)
     2.1 --- a/src/HOL/Fun.thy	Tue May 16 21:32:56 2006 +0200
     2.2 +++ b/src/HOL/Fun.thy	Tue May 16 21:33:01 2006 +0200
     2.3 @@ -48,17 +48,15 @@
     2.4    comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
     2.5    "f o g == %x. f(g(x))"
     2.6  
     2.7 +const_syntax (xsymbols)
     2.8 +  comp  (infixl "\<circ>" 55)
     2.9 +
    2.10 +const_syntax (HTML output)
    2.11 +  comp  (infixl "\<circ>" 55)
    2.12 +
    2.13  text{*compatibility*}
    2.14  lemmas o_def = comp_def
    2.15  
    2.16 -abbreviation (xsymbols)
    2.17 -  comp1  (infixl "\<circ>" 55)
    2.18 -  "comp1 == comp"
    2.19 -
    2.20 -abbreviation (HTML output)
    2.21 -  comp2  (infixl "\<circ>" 55)
    2.22 -  "comp2 == comp"
    2.23 -
    2.24  constdefs
    2.25    inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
    2.26    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     3.1 --- a/src/HOL/HOL.thy	Tue May 16 21:32:56 2006 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue May 16 21:33:01 2006 +0200
     3.3 @@ -52,14 +52,45 @@
     3.4  consts
     3.5    If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
     3.6  
     3.7 +
     3.8  subsubsection {* Additional concrete syntax *}
     3.9  
    3.10 +const_syntax (output)
    3.11 +  "op ="  (infix "=" 50)
    3.12 +
    3.13 +abbreviation
    3.14 +  not_equal     :: "['a, 'a] => bool"               (infixl "~=" 50)
    3.15 +  "x ~= y == ~ (x = y)"
    3.16 +
    3.17 +const_syntax (output)
    3.18 +  not_equal  (infix "~=" 50)
    3.19 +
    3.20 +const_syntax (xsymbols)
    3.21 +  Not  ("\<not> _" [40] 40)
    3.22 +  "op &"  (infixr "\<and>" 35)
    3.23 +  "op |"  (infixr "\<or>" 30)
    3.24 +  "op -->"  (infixr "\<longrightarrow>" 25)
    3.25 +  not_equal  (infix "\<noteq>" 50)
    3.26 +
    3.27 +const_syntax (HTML output)
    3.28 +  Not  ("\<not> _" [40] 40)
    3.29 +  "op &"  (infixr "\<and>" 35)
    3.30 +  "op |"  (infixr "\<or>" 30)
    3.31 +  not_equal  (infix "\<noteq>" 50)
    3.32 +
    3.33 +abbreviation (iff)
    3.34 +  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    3.35 +  "A <-> B == A = B"
    3.36 +
    3.37 +const_syntax (xsymbols)
    3.38 +  iff  (infixr "\<longleftrightarrow>" 25)
    3.39 +
    3.40 +
    3.41  nonterminals
    3.42    letbinds  letbind
    3.43    case_syn  cases_syn
    3.44  
    3.45  syntax
    3.46 -  "_not_equal"  :: "['a, 'a] => bool"                    (infixl "~=" 50)
    3.47    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    3.48  
    3.49    "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
    3.50 @@ -73,7 +104,6 @@
    3.51    "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    3.52  
    3.53  translations
    3.54 -  "x ~= y"                == "~ (x = y)"
    3.55    "THE x. P"              == "The (%x. P)"
    3.56    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    3.57    "let x = a in e"        == "Let a (%x. e)"
    3.58 @@ -85,31 +115,14 @@
    3.59       in Syntax.const "_The" $ x $ t end)]
    3.60  *}
    3.61  
    3.62 -syntax (output)
    3.63 -  "="           :: "['a, 'a] => bool"                    (infix 50)
    3.64 -  "_not_equal"  :: "['a, 'a] => bool"                    (infix "~=" 50)
    3.65 -
    3.66  syntax (xsymbols)
    3.67 -  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    3.68 -  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    3.69 -  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    3.70 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    3.71 -  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    3.72    "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    3.73    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    3.74    "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    3.75    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    3.76  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
    3.77  
    3.78 -syntax (xsymbols output)
    3.79 -  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    3.80 -
    3.81  syntax (HTML output)
    3.82 -  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    3.83 -  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    3.84 -  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    3.85 -  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    3.86 -  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    3.87    "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    3.88    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    3.89    "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    3.90 @@ -119,14 +132,6 @@
    3.91    "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
    3.92    "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
    3.93  
    3.94 -abbreviation (iff)
    3.95 -  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    3.96 -  "A <-> B == A = B"
    3.97 -
    3.98 -abbreviation (xsymbols)
    3.99 -  iff1  (infixr "\<longleftrightarrow>" 25)
   3.100 -  "A \<longleftrightarrow> B == A <-> B"
   3.101 -
   3.102  
   3.103  subsubsection {* Axioms and basic definitions *}
   3.104  
   3.105 @@ -181,6 +186,7 @@
   3.106    The
   3.107    arbitrary
   3.108  
   3.109 +
   3.110  subsubsection {* Generic algebraic operations *}
   3.111  
   3.112  axclass zero < type
     4.1 --- a/src/HOL/Infinite_Set.thy	Tue May 16 21:32:56 2006 +0200
     4.2 +++ b/src/HOL/Infinite_Set.thy	Tue May 16 21:33:01 2006 +0200
     4.3 @@ -346,29 +346,24 @@
     4.4    so we introduce corresponding binders and their proof rules.
     4.5  *}
     4.6  
     4.7 -consts
     4.8 +definition
     4.9    Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
    4.10 +  INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
    4.11    Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
    4.12 -
    4.13 -defs
    4.14 -  INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
    4.15    MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
    4.16  
    4.17 -abbreviation (xsymbols)
    4.18 -  Inf_many1  (binder "\<exists>\<^sub>\<infinity>" 10)
    4.19 -  "Inf_many1 == Inf_many"
    4.20 -  Alm_all1  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.21 -  "Alm_all1 == Alm_all"
    4.22 +const_syntax (xsymbols)
    4.23 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
    4.24 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.25  
    4.26 -abbreviation (HTML output)
    4.27 -  Inf_many2  (binder "\<exists>\<^sub>\<infinity>" 10)
    4.28 -  "Inf_many2 == Inf_many"
    4.29 -  Alm_all2  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.30 -  "Alm_all2 == Alm_all"
    4.31 +const_syntax (HTML output)
    4.32 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
    4.33 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.34  
    4.35  lemma INF_EX:
    4.36    "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
    4.37 -proof (unfold INF_def, rule ccontr)
    4.38 +  unfolding INF_def
    4.39 +proof (rule ccontr)
    4.40    assume inf: "infinite {x. P x}"
    4.41      and notP: "\<not>(\<exists>x. P x)"
    4.42    from notP have "{x. P x} = {}" by simp
    4.43 @@ -418,7 +413,7 @@
    4.44    These simplify the reasoning about deterministic automata.
    4.45  *}
    4.46  
    4.47 -constdefs
    4.48 +definition
    4.49    atmost_one :: "'a set \<Rightarrow> bool"
    4.50    "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
    4.51  
     5.1 --- a/src/HOL/Integ/IntDef.thy	Tue May 16 21:32:56 2006 +0200
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Tue May 16 21:33:01 2006 +0200
     5.3 @@ -567,9 +567,8 @@
     5.4    Nats  :: "'a::comm_semiring_1_cancel set"
     5.5    "Nats == range of_nat"
     5.6  
     5.7 -abbreviation (xsymbols)
     5.8 -  Nats1  ("\<nat>")
     5.9 -  "\<nat> == Nats"
    5.10 +const_syntax (xsymbols)
    5.11 +  Nats  ("\<nat>")
    5.12  
    5.13  lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
    5.14  by (simp add: Nats_def)
    5.15 @@ -701,9 +700,8 @@
    5.16    Ints  :: "'a::comm_ring_1 set"
    5.17    "Ints == range of_int"
    5.18  
    5.19 -abbreviation (xsymbols)
    5.20 -  Ints1  ("\<int>")
    5.21 -  "\<int> == Ints"
    5.22 +const_syntax (xsymbols)
    5.23 +  Ints  ("\<int>")
    5.24  
    5.25  lemma Ints_0 [simp]: "0 \<in> Ints"
    5.26  apply (simp add: Ints_def)
     6.1 --- a/src/HOL/Integ/NatBin.thy	Tue May 16 21:32:56 2006 +0200
     6.2 +++ b/src/HOL/Integ/NatBin.thy	Tue May 16 21:33:01 2006 +0200
     6.3 @@ -24,13 +24,11 @@
     6.4    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
     6.5    "x\<twosuperior> == x^2"
     6.6  
     6.7 -abbreviation (latex output)
     6.8 -  square1  ("(_\<twosuperior>)" [1000] 999)
     6.9 -  "square1 x == x^2"
    6.10 +const_syntax (latex output)
    6.11 +  square  ("(_\<twosuperior>)" [1000] 999)
    6.12  
    6.13 -abbreviation (HTML output)
    6.14 -  square2  ("(_\<twosuperior>)" [1000] 999)
    6.15 -  "square2 x == x^2"
    6.16 +const_syntax (HTML output)
    6.17 +  square  ("(_\<twosuperior>)" [1000] 999)
    6.18  
    6.19  
    6.20  subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
     7.1 --- a/src/HOL/Lambda/Eta.thy	Tue May 16 21:32:56 2006 +0200
     7.2 +++ b/src/HOL/Lambda/Eta.thy	Tue May 16 21:33:01 2006 +0200
     7.3 @@ -228,9 +228,8 @@
     7.4    par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
     7.5    "s =e> t == (s, t) \<in> par_eta"
     7.6  
     7.7 -abbreviation (xsymbols)
     7.8 -  par_eta_red1 :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
     7.9 -  "op \<Rightarrow>\<^sub>\<eta> == op =e>"
    7.10 +const_syntax (xsymbols)
    7.11 +  par_eta_red  (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
    7.12  
    7.13  inductive par_eta
    7.14  intros
    7.15 @@ -300,7 +299,8 @@
    7.16    assumes u: "u => u'"
    7.17    shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
    7.18  proof (induct k fixing: t t')
    7.19 -  case 0 with u show ?case by simp
    7.20 +  case 0
    7.21 +  with u show ?case by simp
    7.22  next
    7.23    case (Suc k)
    7.24    hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]"
    7.25 @@ -387,7 +387,7 @@
    7.26  subsection {* Eta-postponement theorem *}
    7.27  
    7.28  text {*
    7.29 -Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
    7.30 +  Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
    7.31  *}
    7.32  
    7.33  theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
    7.34 @@ -428,7 +428,7 @@
    7.35        and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
    7.36        by (blast dest: par_eta_elim_app par_eta_elim_abs)
    7.37      from beta have "size q' < size t" and "size r' < size t" by simp_all
    7.38 -    with beta(2,3) qq rr obtain t' t'' where "q => t'" and
    7.39 +    with beta(2-3) qq rr obtain t' t'' where "q => t'" and
    7.40        "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
    7.41        by (blast dest: less(1))
    7.42      with s beta show ?thesis
     8.1 --- a/src/HOL/Lambda/Lambda.thy	Tue May 16 21:32:56 2006 +0200
     8.2 +++ b/src/HOL/Lambda/Lambda.thy	Tue May 16 21:33:01 2006 +0200
     8.3 @@ -62,11 +62,9 @@
     8.4    beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
     8.5    "s ->> t == (s, t) \<in> beta^*"
     8.6  
     8.7 -abbreviation (latex)
     8.8 -  beta_red1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     8.9 -  "op \<rightarrow>\<^sub>\<beta> == op ->"
    8.10 -  beta_reds1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    8.11 -  "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
    8.12 +const_syntax (latex)
    8.13 +  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    8.14 +  beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    8.15  
    8.16  inductive beta
    8.17    intros
    8.18 @@ -100,9 +98,7 @@
    8.19  
    8.20  lemma rtrancl_beta_App [intro]:
    8.21      "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
    8.22 -  apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
    8.23 -    intro: rtrancl_trans)
    8.24 -  done
    8.25 +  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
    8.26  
    8.27  
    8.28  subsection {* Substitution-lemmas *}
     9.1 --- a/src/HOL/Lambda/Type.thy	Tue May 16 21:32:56 2006 +0200
     9.2 +++ b/src/HOL/Lambda/Type.thy	Tue May 16 21:33:01 2006 +0200
     9.3 @@ -15,13 +15,11 @@
     9.4    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
     9.5    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
     9.6  
     9.7 -abbreviation (xsymbols)
     9.8 -  shift1  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     9.9 -  "e\<langle>i:a\<rangle> == e<i:a>"
    9.10 +const_syntax (xsymbols)
    9.11 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    9.12  
    9.13 -abbreviation (HTML output)
    9.14 -  shift2  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    9.15 -  "shift2 == shift"
    9.16 +const_syntax (HTML output)
    9.17 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    9.18  
    9.19  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    9.20    by (simp add: shift_def)
    9.21 @@ -62,16 +60,12 @@
    9.22      ("_ ||- _ : _" [50, 50, 50] 50)
    9.23    "env ||- ts : Ts == typings env ts Ts"
    9.24  
    9.25 -abbreviation (xsymbols)
    9.26 -  typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    9.27 -  "env \<turnstile> t : T == env |- t : T"
    9.28 +const_syntax (xsymbols)
    9.29 +  typing_rel  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    9.30  
    9.31 -abbreviation (latex)
    9.32 -  funs2 :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    9.33 -  "op \<Rrightarrow> == op =>>"
    9.34 -  typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.35 -    ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    9.36 -  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
    9.37 +const_syntax (latex)
    9.38 +  funs  (infixr "\<Rrightarrow>" 200)
    9.39 +  typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    9.40  
    9.41  inductive typing
    9.42    intros
    10.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue May 16 21:32:56 2006 +0200
    10.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue May 16 21:33:01 2006 +0200
    10.3 @@ -365,9 +365,8 @@
    10.4    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
    10.5    "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
    10.6  
    10.7 -abbreviation (xsymbols)
    10.8 -  rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
    10.9 -  "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
   10.10 +const_syntax (xsymbols)
   10.11 +  rtyping_rel  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   10.12  
   10.13  inductive rtyping
   10.14    intros
    11.1 --- a/src/HOL/Library/FuncSet.thy	Tue May 16 21:32:56 2006 +0200
    11.2 +++ b/src/HOL/Library/FuncSet.thy	Tue May 16 21:33:01 2006 +0200
    11.3 @@ -23,9 +23,8 @@
    11.4    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
    11.5    "A -> B == Pi A (%_. B)"
    11.6  
    11.7 -abbreviation (xsymbols)
    11.8 -  funcset1  (infixr "\<rightarrow>" 60)
    11.9 -  "funcset1 == funcset"
   11.10 +const_syntax (xsymbols)
   11.11 +  funcset  (infixr "\<rightarrow>" 60)
   11.12  
   11.13  syntax
   11.14    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    12.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Tue May 16 21:32:56 2006 +0200
    12.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Tue May 16 21:33:01 2006 +0200
    12.3 @@ -58,7 +58,7 @@
    12.4    elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
    12.5    "a *o B == {c. EX b:B. c = a * b}"
    12.6  
    12.7 -abbreviation (inout)
    12.8 +abbreviation (input)
    12.9    elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
   12.10    "x =o A == x : A"
   12.11  
    13.1 --- a/src/HOL/Map.thy	Tue May 16 21:32:56 2006 +0200
    13.2 +++ b/src/HOL/Map.thy	Tue May 16 21:33:01 2006 +0200
    13.3 @@ -15,14 +15,20 @@
    13.4  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
    13.5  translations (type) "a ~=> b " <= (type) "a => b option"
    13.6  
    13.7 +syntax (xsymbols)
    13.8 +  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    13.9 +
   13.10  abbreviation
   13.11    empty     ::  "'a ~=> 'b"
   13.12    "empty == %x. None"
   13.13  
   13.14 -constdefs
   13.15 +definition
   13.16    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
   13.17    "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
   13.18  
   13.19 +const_syntax (xsymbols)
   13.20 +  map_comp  (infixl "\<circ>\<^sub>m" 55)
   13.21 +
   13.22  consts
   13.23  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
   13.24  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
   13.25 @@ -32,6 +38,9 @@
   13.26  map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
   13.27  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
   13.28  
   13.29 +const_syntax (latex output)
   13.30 +  restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
   13.31 +
   13.32  nonterminals
   13.33    maplets maplet
   13.34  
   13.35 @@ -44,17 +53,9 @@
   13.36    "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
   13.37  
   13.38  syntax (xsymbols)
   13.39 -  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
   13.40 -
   13.41 -  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
   13.42 -
   13.43    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
   13.44    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
   13.45  
   13.46 -syntax (latex output)
   13.47 -  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
   13.48 -  --"requires amssymb!"
   13.49 -
   13.50  translations
   13.51    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
   13.52    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    14.1 --- a/src/HOL/Orderings.thy	Tue May 16 21:32:56 2006 +0200
    14.2 +++ b/src/HOL/Orderings.thy	Tue May 16 21:33:01 2006 +0200
    14.3 @@ -17,21 +17,23 @@
    14.4  axclass
    14.5    ord < type
    14.6  
    14.7 -syntax
    14.8 -  "less"        :: "['a::ord, 'a] => bool"             ("op <")
    14.9 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("op <=")
   14.10 -
   14.11  consts
   14.12 -  "less"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
   14.13 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
   14.14 +  less  :: "['a::ord, 'a] => bool"
   14.15 +  less_eq  :: "['a::ord, 'a] => bool"
   14.16  
   14.17 -syntax (xsymbols)
   14.18 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
   14.19 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
   14.20 +const_syntax
   14.21 +  less  ("op <")
   14.22 +  less  ("(_/ < _)"  [50, 51] 50)
   14.23 +  less_eq  ("op <=")
   14.24 +  less_eq  ("(_/ <= _)" [50, 51] 50)
   14.25  
   14.26 -syntax (HTML output)
   14.27 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
   14.28 -  "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
   14.29 +const_syntax (xsymbols)
   14.30 +  less_eq  ("op \<le>")
   14.31 +  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
   14.32 +
   14.33 +const_syntax (HTML output)
   14.34 +  less_eq  ("op \<le>")
   14.35 +  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
   14.36  
   14.37  abbreviation (input)
   14.38    greater  (infixl ">" 50)
   14.39 @@ -39,13 +41,8 @@
   14.40    greater_eq  (infixl ">=" 50)
   14.41    "x >= y == y <= x"
   14.42  
   14.43 -abbreviation (xsymbols)
   14.44 -  greater_eq1  (infixl "\<ge>" 50)
   14.45 -  "x \<ge> y == x >= y"
   14.46 -
   14.47 -abbreviation (HTML output)
   14.48 -  greater_eq2  (infixl "\<ge>" 50)
   14.49 -  "greater_eq2 == greater_eq"
   14.50 +const_syntax (xsymbols)
   14.51 +  greater_eq  (infixl "\<ge>" 50)
   14.52  
   14.53  
   14.54  subsection {* Monotonicity *}
    15.1 --- a/src/HOL/Product_Type.thy	Tue May 16 21:32:56 2006 +0200
    15.2 +++ b/src/HOL/Product_Type.thy	Tue May 16 21:33:01 2006 +0200
    15.3 @@ -113,13 +113,11 @@
    15.4    Times :: "['a set, 'b set] => ('a * 'b) set"  (infixr "<*>" 80)
    15.5    "A <*> B == Sigma A (%_. B)"
    15.6  
    15.7 -abbreviation (xsymbols)
    15.8 -  Times1  (infixr "\<times>" 80)
    15.9 -  "Times1 == Times"
   15.10 +const_syntax (xsymbols)
   15.11 +  Times  (infixr "\<times>" 80)
   15.12  
   15.13 -abbreviation (HTML output)
   15.14 -  Times2  (infixr "\<times>" 80)
   15.15 -  "Times2 == Times"
   15.16 +const_syntax (HTML output)
   15.17 +  Times  (infixr "\<times>" 80)
   15.18  
   15.19  
   15.20  subsubsection {* Concrete syntax *}
    16.1 --- a/src/HOL/Relation.thy	Tue May 16 21:32:56 2006 +0200
    16.2 +++ b/src/HOL/Relation.thy	Tue May 16 21:33:01 2006 +0200
    16.3 @@ -12,13 +12,14 @@
    16.4  
    16.5  subsection {* Definitions *}
    16.6  
    16.7 -constdefs
    16.8 +definition
    16.9    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
   16.10    "r^-1 == {(y, x). (x, y) : r}"
   16.11 -syntax (xsymbols)
   16.12 -  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\<inverse>)" [1000] 999)
   16.13  
   16.14 -constdefs
   16.15 +const_syntax (xsymbols)
   16.16 +  converse  ("(_\<inverse>)" [1000] 999)
   16.17 +
   16.18 +definition
   16.19    rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
   16.20    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
   16.21  
    17.1 --- a/src/HOL/Set.thy	Tue May 16 21:32:56 2006 +0200
    17.2 +++ b/src/HOL/Set.thy	Tue May 16 21:33:01 2006 +0200
    17.3 @@ -34,11 +34,11 @@
    17.4    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    17.5    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    17.6    image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
    17.7 -
    17.8 -syntax
    17.9 -  "op :"        :: "'a => 'a set => bool"                ("op :")
   17.10 -consts
   17.11 -  "op :"        :: "'a => 'a set => bool"                ("(_/ : _)" [50, 51] 50)  -- "membership"
   17.12 +  "op :"        :: "'a => 'a set => bool"                -- "membership"
   17.13 +
   17.14 +const_syntax
   17.15 +  "op :"  ("op :")
   17.16 +  "op :"  ("(_/ : _)" [50, 51] 50)
   17.17  
   17.18  local
   17.19  
   17.20 @@ -51,10 +51,62 @@
   17.21    range :: "('a => 'b) => 'b set"             -- "of function"
   17.22    "range f == f ` UNIV"
   17.23  
   17.24 +abbreviation
   17.25 +  "not_mem x A == ~ (x : A)"                  -- "non-membership"
   17.26 +
   17.27 +const_syntax
   17.28 +  not_mem  ("op ~:")
   17.29 +  not_mem  ("(_/ ~: _)" [50, 51] 50)
   17.30 +
   17.31 +const_syntax (xsymbols)
   17.32 +  "op Int"  (infixl "\<inter>" 70)
   17.33 +  "op Un"  (infixl "\<union>" 65)
   17.34 +  "op :"  ("op \<in>")
   17.35 +  "op :"  ("(_/ \<in> _)" [50, 51] 50)
   17.36 +  not_mem  ("op \<notin>")
   17.37 +  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
   17.38 +  Union  ("\<Union>_" [90] 90)
   17.39 +  Inter  ("\<Inter>_" [90] 90)
   17.40 +
   17.41 +const_syntax (HTML output)
   17.42 +  "op Int"  (infixl "\<inter>" 70)
   17.43 +  "op Un"  (infixl "\<union>" 65)
   17.44 +  "op :"  ("op \<in>")
   17.45 +  "op :"  ("(_/ \<in> _)" [50, 51] 50)
   17.46 +  not_mem  ("op \<notin>")
   17.47 +  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
   17.48 +
   17.49 +abbreviation
   17.50 +  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   17.51 +  "subset == less"
   17.52 +  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   17.53 +  "subset_eq == less_eq"
   17.54 +
   17.55 +const_syntax (output)
   17.56 +  subset  ("op <")
   17.57 +  subset  ("(_/ < _)" [50, 51] 50)
   17.58 +  subset_eq  ("op <=")
   17.59 +  subset_eq  ("(_/ <= _)" [50, 51] 50)
   17.60 +
   17.61 +const_syntax (xsymbols)
   17.62 +  subset  ("op \<subset>")
   17.63 +  subset  ("(_/ \<subset> _)" [50, 51] 50)
   17.64 +  subset_eq  ("op \<subseteq>")
   17.65 +  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
   17.66 +
   17.67 +const_syntax (HTML output)
   17.68 +  subset  ("op \<subset>")
   17.69 +  subset  ("(_/ \<subset> _)" [50, 51] 50)
   17.70 +  subset_eq  ("op \<subseteq>")
   17.71 +  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
   17.72 +
   17.73 +abbreviation (input)
   17.74 +  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infixl "\<supset>" 50)
   17.75 +  "supset == greater"
   17.76 +  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "\<supseteq>" 50)
   17.77 +  "supset_eq == greater_eq"
   17.78 +
   17.79  syntax
   17.80 -  "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
   17.81 -  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
   17.82 -
   17.83    "@Finset"     :: "args => 'a set"                       ("{(_)}")
   17.84    "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
   17.85    "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
   17.86 @@ -63,18 +115,15 @@
   17.87    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
   17.88    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
   17.89    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
   17.90 -
   17.91    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   17.92    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   17.93    "_Bleast"       :: "id => 'a set => bool => 'a"      ("(3LEAST _:_./ _)" [0, 0, 10] 10)
   17.94  
   17.95 -
   17.96  syntax (HOL)
   17.97    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   17.98    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   17.99  
  17.100  translations
  17.101 -  "x ~: y"      == "~ (x : y)"
  17.102    "{x, xs}"     == "insert x {xs}"
  17.103    "{x}"         == "insert x {}"
  17.104    "{x. P}"      == "Collect (%x. P)"
  17.105 @@ -91,41 +140,12 @@
  17.106    "EX x:A. P"   == "Bex A (%x. P)"
  17.107    "LEAST x:A. P" => "LEAST x. x:A & P"
  17.108  
  17.109 -
  17.110 -syntax (output)
  17.111 -  "_setle"      :: "'a set => 'a set => bool"             ("op <=")
  17.112 -  "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
  17.113 -  "_setless"    :: "'a set => 'a set => bool"             ("op <")
  17.114 -  "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
  17.115 -
  17.116  syntax (xsymbols)
  17.117 -  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
  17.118 -  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
  17.119 -  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
  17.120 -  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
  17.121 -  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
  17.122 -  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
  17.123 -  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
  17.124 -  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
  17.125 -  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
  17.126 -  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
  17.127 -  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
  17.128 -  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
  17.129    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
  17.130    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
  17.131    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
  17.132  
  17.133  syntax (HTML output)
  17.134 -  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
  17.135 -  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
  17.136 -  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
  17.137 -  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
  17.138 -  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
  17.139 -  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
  17.140 -  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
  17.141 -  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
  17.142 -  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
  17.143 -  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
  17.144    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
  17.145    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
  17.146  
  17.147 @@ -135,47 +155,25 @@
  17.148    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
  17.149    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
  17.150    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
  17.151 -(*
  17.152 -syntax (xsymbols)
  17.153 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
  17.154 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
  17.155 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
  17.156 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
  17.157 -*)
  17.158 +
  17.159  syntax (latex output)
  17.160    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
  17.161    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
  17.162    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
  17.163    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
  17.164  
  17.165 -text{* Note the difference between ordinary xsymbol syntax of indexed
  17.166 -unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
  17.167 -and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
  17.168 -former does not make the index expression a subscript of the
  17.169 -union/intersection symbol because this leads to problems with nested
  17.170 -subscripts in Proof General.  *}
  17.171 -
  17.172 -
  17.173 -translations
  17.174 -  "op \<subseteq>" => "op <= :: _ set => _ set => bool"
  17.175 -  "op \<subset>" => "op <  :: _ set => _ set => bool"
  17.176 -
  17.177 -typed_print_translation {*
  17.178 -  let
  17.179 -    fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
  17.180 -          list_comb (Syntax.const "_setle", ts)
  17.181 -      | le_tr' _ _ _ = raise Match;
  17.182 -
  17.183 -    fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
  17.184 -          list_comb (Syntax.const "_setless", ts)
  17.185 -      | less_tr' _ _ _ = raise Match;
  17.186 -  in [("less_eq", le_tr'), ("less", less_tr')] end
  17.187 -*}
  17.188 +text{*
  17.189 +  Note the difference between ordinary xsymbol syntax of indexed
  17.190 +  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
  17.191 +  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
  17.192 +  former does not make the index expression a subscript of the
  17.193 +  union/intersection symbol because this leads to problems with nested
  17.194 +  subscripts in Proof General. *}
  17.195  
  17.196  
  17.197  subsubsection "Bounded quantifiers"
  17.198  
  17.199 -syntax
  17.200 +syntax (output)
  17.201    "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
  17.202    "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
  17.203    "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
  17.204 @@ -187,7 +185,7 @@
  17.205    "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
  17.206    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
  17.207  
  17.208 -syntax (HOL)
  17.209 +syntax (HOL output)
  17.210    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
  17.211    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
  17.212    "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
    18.1 --- a/src/HOL/Transitive_Closure.thy	Tue May 16 21:32:56 2006 +0200
    18.2 +++ b/src/HOL/Transitive_Closure.thy	Tue May 16 21:33:01 2006 +0200
    18.3 @@ -36,20 +36,19 @@
    18.4      r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
    18.5      trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    18.6  
    18.7 -syntax
    18.8 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    18.9 -translations
   18.10 -  "r^=" == "r \<union> Id"
   18.11 +abbreviation
   18.12 +  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
   18.13 +  "r^= == r \<union> Id"
   18.14  
   18.15 -syntax (xsymbols)
   18.16 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
   18.17 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
   18.18 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
   18.19 +const_syntax (xsymbols)
   18.20 +  rtrancl  ("(_\<^sup>*)" [1000] 999)
   18.21 +  trancl  ("(_\<^sup>+)" [1000] 999)
   18.22 +  reflcl  ("(_\<^sup>=)" [1000] 999)
   18.23  
   18.24 -syntax (HTML output)
   18.25 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
   18.26 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
   18.27 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
   18.28 +const_syntax (HTML output)
   18.29 +  rtrancl  ("(_\<^sup>*)" [1000] 999)
   18.30 +  trancl  ("(_\<^sup>+)" [1000] 999)
   18.31 +  reflcl  ("(_\<^sup>=)" [1000] 999)
   18.32  
   18.33  
   18.34  subsection {* Reflexive-transitive closure *}