src/HOL/Complete_Lattice.thy
changeset 35115 446c5063e4fd
parent 34007 aea892559fc5
child 35629 57f1a5e93b6b
     1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -106,10 +106,10 @@
     1.4    "INF x. B"     == "INF x:CONST UNIV. B"
     1.5    "INF x:A. B"   == "CONST INFI A (%x. B)"
     1.6  
     1.7 -print_translation {* [
     1.8 -Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
     1.9 -Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
    1.10 -] *} -- {* to avoid eta-contraction of body *}
    1.11 +print_translation {*
    1.12 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"},
    1.13 +    Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}]
    1.14 +*} -- {* to avoid eta-contraction of body *}
    1.15  
    1.16  context complete_lattice
    1.17  begin
    1.18 @@ -282,16 +282,16 @@
    1.19    "UNION \<equiv> SUPR"
    1.20  
    1.21  syntax
    1.22 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.23 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    1.24 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.25 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    1.26  
    1.27  syntax (xsymbols)
    1.28 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    1.29 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    1.30 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    1.31 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    1.32  
    1.33  syntax (latex output)
    1.34 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.35 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.36 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.37 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.38  
    1.39  translations
    1.40    "UN x y. B"   == "UN x. UN y. B"
    1.41 @@ -308,9 +308,9 @@
    1.42    subscripts in Proof General.
    1.43  *}
    1.44  
    1.45 -print_translation {* [
    1.46 -Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
    1.47 -] *} -- {* to avoid eta-contraction of body *}
    1.48 +print_translation {*
    1.49 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
    1.50 +*} -- {* to avoid eta-contraction of body *}
    1.51  
    1.52  lemma UNION_eq_Union_image:
    1.53    "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
    1.54 @@ -518,16 +518,16 @@
    1.55    "INTER \<equiv> INFI"
    1.56  
    1.57  syntax
    1.58 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.59 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    1.60 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.61 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    1.62  
    1.63  syntax (xsymbols)
    1.64 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    1.65 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    1.66 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    1.67 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    1.68  
    1.69  syntax (latex output)
    1.70 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.71 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.72 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.73 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.74  
    1.75  translations
    1.76    "INT x y. B"  == "INT x. INT y. B"
    1.77 @@ -535,9 +535,9 @@
    1.78    "INT x. B"    == "INT x:CONST UNIV. B"
    1.79    "INT x:A. B"  == "CONST INTER A (%x. B)"
    1.80  
    1.81 -print_translation {* [
    1.82 -Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
    1.83 -] *} -- {* to avoid eta-contraction of body *}
    1.84 +print_translation {*
    1.85 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    1.86 +*} -- {* to avoid eta-contraction of body *}
    1.87  
    1.88  lemma INTER_eq_Inter_image:
    1.89    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"