replaced syntax/translations by abbreviation;
authorwenzelm
Tue May 02 20:42:32 2006 +0200 (2006-05-02)
changeset 195361a3a3cf8b4fa
parent 19535 e4fdeb32eadf
child 19537 213ff8b0c60c
replaced syntax/translations by abbreviation;
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Library/FuncSet.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Fun.thy	Tue May 02 20:42:30 2006 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue May 02 20:42:32 2006 +0200
     1.3 @@ -39,23 +39,25 @@
     1.4  *)
     1.5  
     1.6  constdefs
     1.7 - override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
     1.8 -"override_on f g A == %a. if a : A then g a else f a"
     1.9 +  override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
    1.10 +  "override_on f g A == %a. if a : A then g a else f a"
    1.11  
    1.12 - id :: "'a => 'a"
    1.13 -"id == %x. x"
    1.14 +  id :: "'a => 'a"
    1.15 +  "id == %x. x"
    1.16  
    1.17 - comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.18 -"f o g == %x. f(g(x))"
    1.19 +  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.20 +  "f o g == %x. f(g(x))"
    1.21  
    1.22  text{*compatibility*}
    1.23  lemmas o_def = comp_def
    1.24  
    1.25 -syntax (xsymbols)
    1.26 -  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
    1.27 -syntax (HTML output)
    1.28 -  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
    1.29 +abbreviation (xsymbols)
    1.30 +  comp1  (infixl "\<circ>" 55)
    1.31 +  "comp1 == comp"
    1.32  
    1.33 +abbreviation (HTML output)
    1.34 +  comp2  (infixl "\<circ>" 55)
    1.35 +  "comp2 == comp"
    1.36  
    1.37  constdefs
    1.38    inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
     2.1 --- a/src/HOL/HOL.thy	Tue May 02 20:42:30 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue May 02 20:42:32 2006 +0200
     2.3 @@ -119,21 +119,13 @@
     2.4    "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
     2.5    "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
     2.6  
     2.7 -syntax
     2.8 -  "_iff" :: "bool => bool => bool"                       (infixr "<->" 25)
     2.9 -syntax (xsymbols)
    2.10 -  "_iff" :: "bool => bool => bool"                       (infixr "\<longleftrightarrow>" 25)
    2.11 -translations
    2.12 -  "op <->" => "op = :: bool => bool => bool"
    2.13 +abbreviation (iff)
    2.14 +  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    2.15 +  "A <-> B == A = B"
    2.16  
    2.17 -typed_print_translation {*
    2.18 -  let
    2.19 -    fun iff_tr' _ (Type ("fun", (Type ("bool", _) :: _))) ts =
    2.20 -          if Output.has_mode "iff" then Term.list_comb (Syntax.const "_iff", ts)
    2.21 -          else raise Match
    2.22 -      | iff_tr' _ _ _ = raise Match;
    2.23 -  in [("op =", iff_tr')] end
    2.24 -*}
    2.25 +abbreviation (xsymbols)
    2.26 +  iff1  (infixr "\<longleftrightarrow>" 25)
    2.27 +  "A \<longleftrightarrow> B == A <-> B"
    2.28  
    2.29  
    2.30  subsubsection {* Axioms and basic definitions *}
     3.1 --- a/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:30 2006 +0200
     3.2 +++ b/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:32 2006 +0200
     3.3 @@ -19,14 +19,20 @@
     3.4    "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
     3.5    "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
     3.6  
     3.7 +abbreviation
     3.8 +  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
     3.9 +  "A -> B == Pi A (%_. B)"
    3.10 +
    3.11 +abbreviation (xsymbols)
    3.12 +  funcset1  (infixr "\<rightarrow>" 60)
    3.13 +  "funcset1 == funcset"
    3.14 +
    3.15  syntax
    3.16    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    3.17 -  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
    3.18    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    3.19  
    3.20  syntax (xsymbols)
    3.21    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    3.22 -  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
    3.23    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    3.24  
    3.25  syntax (HTML output)
    3.26 @@ -34,16 +40,13 @@
    3.27    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    3.28  
    3.29  translations
    3.30 -  "PI x:A. B" => "Pi A (%x. B)"
    3.31 -  "A -> B" => "Pi A (%_. B)"
    3.32 +  "PI x:A. B" == "Pi A (%x. B)"
    3.33    "%x:A. f" == "restrict (%x. f) A"
    3.34  
    3.35  constdefs
    3.36    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    3.37    "compose A g f == \<lambda>x\<in>A. g (f x)"
    3.38  
    3.39 -print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
    3.40 -
    3.41  
    3.42  subsection{*Basic Properties of @{term Pi}*}
    3.43  
     4.1 --- a/src/HOL/Orderings.thy	Tue May 02 20:42:30 2006 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Tue May 02 20:42:32 2006 +0200
     4.3 @@ -33,20 +33,19 @@
     4.4    "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
     4.5    "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
     4.6  
     4.7 -text{* Syntactic sugar: *}
     4.8 +abbreviation (input)
     4.9 +  greater  (infixl ">" 50)
    4.10 +  "x > y == y < x"
    4.11 +  greater_eq  (infixl ">=" 50)
    4.12 +  "x >= y == y <= x"
    4.13  
    4.14 -syntax
    4.15 -  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    4.16 -  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    4.17 -translations
    4.18 -  "x > y"  => "y < x"
    4.19 -  "x >= y" => "y <= x"
    4.20 +abbreviation (xsymbols)
    4.21 +  greater_eq1  (infixl "\<ge>" 50)
    4.22 +  "x \<ge> y == x >= y"
    4.23  
    4.24 -syntax (xsymbols)
    4.25 -  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    4.26 -
    4.27 -syntax (HTML output)
    4.28 -  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    4.29 +abbreviation (HTML output)
    4.30 +  greater_eq2  (infixl "\<ge>" 50)
    4.31 +  "greater_eq2 == greater_eq"
    4.32  
    4.33  
    4.34  subsection {* Monotonicity *}