# HG changeset patch
# User wenzelm
# Date 1146595352 -7200
# Node ID 1a3a3cf8b4faabbb72ec0ed13abf9fb57933ebbb
# Parent  e4fdeb32eadfc0fe1fb4960a643a13f247761799
replaced syntax/translations by abbreviation;

diff -r e4fdeb32eadf -r 1a3a3cf8b4fa src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 02 20:42:30 2006 +0200
+++ b/src/HOL/Fun.thy	Tue May 02 20:42:32 2006 +0200
@@ -39,23 +39,25 @@
 *)
 
 constdefs
- override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
-"override_on f g A == %a. if a : A then g a else f a"
+  override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
+  "override_on f g A == %a. if a : A then g a else f a"
 
- id :: "'a => 'a"
-"id == %x. x"
+  id :: "'a => 'a"
+  "id == %x. x"
 
- comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
-"f o g == %x. f(g(x))"
+  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
+  "f o g == %x. f(g(x))"
 
 text{*compatibility*}
 lemmas o_def = comp_def
 
-syntax (xsymbols)
-  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
-syntax (HTML output)
-  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
+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*)
diff -r e4fdeb32eadf -r 1a3a3cf8b4fa src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 02 20:42:30 2006 +0200
+++ b/src/HOL/HOL.thy	Tue May 02 20:42:32 2006 +0200
@@ -119,21 +119,13 @@
   "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
 
-syntax
-  "_iff" :: "bool => bool => bool"                       (infixr "<->" 25)
-syntax (xsymbols)
-  "_iff" :: "bool => bool => bool"                       (infixr "\<longleftrightarrow>" 25)
-translations
-  "op <->" => "op = :: bool => bool => bool"
+abbreviation (iff)
+  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
+  "A <-> B == A = B"
 
-typed_print_translation {*
-  let
-    fun iff_tr' _ (Type ("fun", (Type ("bool", _) :: _))) ts =
-          if Output.has_mode "iff" then Term.list_comb (Syntax.const "_iff", ts)
-          else raise Match
-      | iff_tr' _ _ _ = raise Match;
-  in [("op =", iff_tr')] end
-*}
+abbreviation (xsymbols)
+  iff1  (infixr "\<longleftrightarrow>" 25)
+  "A \<longleftrightarrow> B == A <-> B"
 
 
 subsubsection {* Axioms and basic definitions *}
diff -r e4fdeb32eadf -r 1a3a3cf8b4fa src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:30 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:32 2006 +0200
@@ -19,14 +19,20 @@
   "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
   "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
 
+abbreviation
+  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
+  "A -> B == Pi A (%_. B)"
+
+abbreviation (xsymbols)
+  funcset1  (infixr "\<rightarrow>" 60)
+  "funcset1 == funcset"
+
 syntax
   "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
-  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
 
 syntax (xsymbols)
   "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
-  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 syntax (HTML output)
@@ -34,16 +40,13 @@
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 translations
-  "PI x:A. B" => "Pi A (%x. B)"
-  "A -> B" => "Pi A (%_. B)"
+  "PI x:A. B" == "Pi A (%x. B)"
   "%x:A. f" == "restrict (%x. f) A"
 
 constdefs
   "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
   "compose A g f == \<lambda>x\<in>A. g (f x)"
 
-print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
-
 
 subsection{*Basic Properties of @{term Pi}*}
 
diff -r e4fdeb32eadf -r 1a3a3cf8b4fa src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue May 02 20:42:30 2006 +0200
+++ b/src/HOL/Orderings.thy	Tue May 02 20:42:32 2006 +0200
@@ -33,20 +33,19 @@
   "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
   "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
 
-text{* Syntactic sugar: *}
+abbreviation (input)
+  greater  (infixl ">" 50)
+  "x > y == y < x"
+  greater_eq  (infixl ">=" 50)
+  "x >= y == y <= x"
 
-syntax
-  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
-  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
-translations
-  "x > y"  => "y < x"
-  "x >= y" => "y <= x"
+abbreviation (xsymbols)
+  greater_eq1  (infixl "\<ge>" 50)
+  "x \<ge> y == x >= y"
 
-syntax (xsymbols)
-  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
-
-syntax (HTML output)
-  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
+abbreviation (HTML output)
+  greater_eq2  (infixl "\<ge>" 50)
+  "greater_eq2 == greater_eq"
 
 
 subsection {* Monotonicity *}