nipkow@15469: (*  Title:      HOL/Library/OptionalSugar.thy
hoelzl@55052:     Author:     Gerwin Klein, Tobias Nipkow
nipkow@15469:     Copyright   2005 NICTA and TUM
nipkow@15469: *)
nipkow@15476: (*<*)
nipkow@15469: theory OptionalSugar
haftmann@30663: imports Complex_Main LaTeXsugar
nipkow@15469: begin
nipkow@15469: 
nipkow@30474: (* hiding set *)
nipkow@22835: translations
wenzelm@30404:   "xs" <= "CONST set xs"
nipkow@22835: 
nipkow@30474: (* hiding numeric conversions - embeddings only *)
nipkow@30474: translations
nipkow@30474:   "n" <= "CONST of_nat n"
nipkow@30474:   "n" <= "CONST int n"
wenzelm@35115:   "n" <= "CONST real n"
nipkow@30474:   "n" <= "CONST real_of_nat n"
nipkow@30474:   "n" <= "CONST real_of_int n"
nipkow@30502:   "n" <= "CONST of_real n"
nipkow@30502:   "n" <= "CONST complex_of_real n"
nipkow@30474: 
nipkow@15469: (* append *)
nipkow@15469: syntax (latex output)
wenzelm@35115:   "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
nipkow@15469: translations
wenzelm@35115:   "_appendL xs ys" <= "xs @ ys" 
wenzelm@35115:   "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
nipkow@15469: 
nipkow@15469: 
haftmann@32891: (* deprecated, use thm with style instead, will be removed *)
nipkow@15469: (* aligning equations *)
wenzelm@21210: notation (tab output)
haftmann@38864:   "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
wenzelm@56245:   "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
nipkow@15469: 
nipkow@15469: (* Let *)
nipkow@15469: translations 
wenzelm@35250:   "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
wenzelm@35250:   "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
nipkow@15469: 
nipkow@15469:   "_tuple_args x (_tuple_args y z)" ==
nipkow@15469:     "_tuple_args x (_tuple_arg (_tuple y z))"
nipkow@15469: 
wenzelm@35250:   "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
wenzelm@35250:   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
wenzelm@35250:   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
nipkow@15469: 
haftmann@29494: (* type constraints with spacing *)
wenzelm@55038: 
wenzelm@55038: no_syntax (xsymbols output)
wenzelm@55038:   "_constrain" :: "logic => type => logic"  ("_\<Colon>_" [4, 0] 3)
wenzelm@55038:   "_constrain" :: "prop' => type => prop'"  ("_\<Colon>_" [4, 0] 3)
wenzelm@55038: 
wenzelm@55038: syntax (xsymbols output)
wenzelm@55038:   "_constrain" :: "logic => type => logic"  ("_ \<Colon> _" [4, 0] 3)
wenzelm@55038:   "_constrain" :: "prop' => type => prop'"  ("_ \<Colon> _" [4, 0] 3)
wenzelm@55038: 
haftmann@29494: 
haftmann@29494: (* sorts as intersections *)
wenzelm@55038: 
wenzelm@55038: syntax (xsymbols output)
wenzelm@55038:   "_topsort" :: "sort"  ("\<top>" 1000)
wenzelm@55038:   "_sort" :: "classes => sort"  ("'(_')" 1000)
wenzelm@55038:   "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
wenzelm@55038:   "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
nipkow@15469: 
nipkow@15476: end
nipkow@15476: (*>*)