src/HOL/HOL.thy
changeset 46125 00cd193a48dc
parent 45654 cf10bde35973
child 46161 4ed94d92ae19
     1.1 --- a/src/HOL/HOL.thy	Thu Jan 05 15:31:49 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Jan 05 18:18:39 2012 +0100
     1.3 @@ -104,34 +104,31 @@
     1.4  notation (xsymbols)
     1.5    iff  (infixr "\<longleftrightarrow>" 25)
     1.6  
     1.7 -nonterminal letbinds and letbind
     1.8 -nonterminal case_pat and case_syn and cases_syn
     1.9 +syntax
    1.10 +  "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.11 +translations
    1.12 +  "THE x. P" == "CONST The (%x. P)"
    1.13 +print_translation {*
    1.14 +  [(@{const_syntax The}, fn [Abs abs] =>
    1.15 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.16 +      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    1.17 +*}  -- {* To avoid eta-contraction of body *}
    1.18  
    1.19 +nonterminal letbinds and letbind
    1.20  syntax
    1.21 -  "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    1.22 -
    1.23    "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
    1.24    ""            :: "letbind => letbinds"                 ("_")
    1.25    "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
    1.26    "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
    1.27  
    1.28 -  "_case_syntax"      :: "['a, cases_syn] => 'b"              ("(case _ of/ _)" 10)
    1.29 -  "_case1"            :: "[case_pat, 'b] => case_syn"         ("(2_ =>/ _)" 10)
    1.30 -  ""                  :: "case_syn => cases_syn"              ("_")
    1.31 -  "_case2"            :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
    1.32 -  "_strip_positions"  :: "'a => case_pat"                     ("_")
    1.33 -
    1.34 +nonterminal case_syn and cases_syn
    1.35 +syntax
    1.36 +  "_case_syntax" :: "['a, cases_syn] => 'b"  ("(case _ of/ _)" 10)
    1.37 +  "_case1" :: "['a, 'b] => case_syn"  ("(2_ =>/ _)" 10)
    1.38 +  "" :: "case_syn => cases_syn"  ("_")
    1.39 +  "_case2" :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    1.40  syntax (xsymbols)
    1.41 -  "_case1" :: "[case_pat, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    1.42 -
    1.43 -translations
    1.44 -  "THE x. P"              == "CONST The (%x. P)"
    1.45 -
    1.46 -print_translation {*
    1.47 -  [(@{const_syntax The}, fn [Abs abs] =>
    1.48 -      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.49 -      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    1.50 -*}  -- {* To avoid eta-contraction of body *}
    1.51 +  "_case1" :: "['a, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    1.52  
    1.53  notation (xsymbols)
    1.54    All  (binder "\<forall>" 10) and