isabelle: src/HOL/Library/OptionalSugar.thy@26d1c71784f1 (annotated)

15469 f5d22f504ab9 new nipkow parents: diff changeset	1	(* Title: HOL/Library/OptionalSugar.thy
55052 c602013f127e spelling hoelzl parents: 55038 diff changeset	2	Author: Gerwin Klein, Tobias Nipkow
15469 f5d22f504ab9 new nipkow parents: diff changeset	3	Copyright 2005 NICTA and TUM
f5d22f504ab9 new nipkow parents: diff changeset	4	*)
15476 b8cb20cc0c0b fixed bugs nipkow parents: 15469 diff changeset	5	(<)
15469 f5d22f504ab9 new nipkow parents: diff changeset	6	theory OptionalSugar
30663 0b6aff7451b2 Main is (Complex_Main) base entry point in library theories haftmann parents: 30503 diff changeset	7	imports Complex_Main LaTeXsugar
15469 f5d22f504ab9 new nipkow parents: diff changeset	8	begin
f5d22f504ab9 new nipkow parents: diff changeset	9
30474 52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	10	(* hiding set *)
22835 37d3a984d730 added "set" supression nipkow parents: 21404 diff changeset	11	translations
30404 d03dd6301678 more robust treatment of (authentic) consts within translations; wenzelm parents: 29494 diff changeset	12	"xs" <= "CONST set xs"
22835 37d3a984d730 added "set" supression nipkow parents: 21404 diff changeset	13
30474 52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	14	(* hiding numeric conversions - embeddings only *)
52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	15	translations
52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	16	"n" <= "CONST of_nat n"
52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	17	"n" <= "CONST int n"
35115 446c5063e4fd modernized translations; wenzelm parents: 33384 diff changeset	18	"n" <= "CONST real n"
30474 52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	19	"n" <= "CONST real_of_nat n"
52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	20	"n" <= "CONST real_of_int n"
30502 b80d2621caee hiding numeric coercions in LaTeX nipkow parents: 30474 diff changeset	21	"n" <= "CONST of_real n"
b80d2621caee hiding numeric coercions in LaTeX nipkow parents: 30474 diff changeset	22	"n" <= "CONST complex_of_real n"
30474 52e92009aacb optional latex sugar nipkow parents: 30404 diff changeset	23
15469 f5d22f504ab9 new nipkow parents: diff changeset	24	(* append *)
f5d22f504ab9 new nipkow parents: diff changeset	25	syntax (latex output)
35115 446c5063e4fd modernized translations; wenzelm parents: 33384 diff changeset	26	"_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
15469 f5d22f504ab9 new nipkow parents: diff changeset	27	translations
35115 446c5063e4fd modernized translations; wenzelm parents: 33384 diff changeset	28	"_appendL xs ys" <= "xs @ ys"
446c5063e4fd modernized translations; wenzelm parents: 33384 diff changeset	29	"_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
15469 f5d22f504ab9 new nipkow parents: diff changeset	30
f5d22f504ab9 new nipkow parents: diff changeset	31
32891 d403b99287ff new generalized concept for term styles haftmann parents: 30663 diff changeset	32	(* deprecated, use thm with style instead, will be removed *)
15469 f5d22f504ab9 new nipkow parents: diff changeset	33	(* aligning equations *)
21210 c17fd2df4e9e renamed 'const_syntax' to 'notation'; wenzelm parents: 19674 diff changeset	34	notation (tab output)
38864 4abe644fcea5 formerly unnamed infix equality now named HOL.eq haftmann parents: 35250 diff changeset	35	"HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
56245 84fc7dfa3cd4 more qualified names; wenzelm parents: 55052 diff changeset	36	"Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
15469 f5d22f504ab9 new nipkow parents: diff changeset	37
f5d22f504ab9 new nipkow parents: diff changeset	38	(* Let *)
f5d22f504ab9 new nipkow parents: diff changeset	39	translations
35250 92664dca6f20 proper markup of const syntax; wenzelm parents: 35115 diff changeset	40	"_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
92664dca6f20 proper markup of const syntax; wenzelm parents: 35115 diff changeset	41	"_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
15469 f5d22f504ab9 new nipkow parents: diff changeset	42
f5d22f504ab9 new nipkow parents: diff changeset	43	"_tuple_args x (_tuple_args y z)" ==
f5d22f504ab9 new nipkow parents: diff changeset	44	"_tuple_args x (_tuple_arg (_tuple y z))"
f5d22f504ab9 new nipkow parents: diff changeset	45
35250 92664dca6f20 proper markup of const syntax; wenzelm parents: 35115 diff changeset	46	"_bind (CONST Some p) e" <= "_bind p (CONST the e)"
92664dca6f20 proper markup of const syntax; wenzelm parents: 35115 diff changeset	47	"_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
92664dca6f20 proper markup of const syntax; wenzelm parents: 35115 diff changeset	48	"_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
15469 f5d22f504ab9 new nipkow parents: diff changeset	49
29494 a189c6274c7a type constraints and sort intersection haftmann parents: 22835 diff changeset	50	(* type constraints with spacing *)
55038 f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	51
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	52	no_syntax (xsymbols output)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	53	"_constrain" :: "logic => type => logic" ("_\<Colon>_" [4, 0] 3)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	54	"_constrain" :: "prop' => type => prop'" ("_\<Colon>_" [4, 0] 3)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	55
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	56	syntax (xsymbols output)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	57	"_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	58	"_constrain" :: "prop' => type => prop'" ("_ \<Colon> _" [4, 0] 3)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	59
29494 a189c6274c7a type constraints and sort intersection haftmann parents: 22835 diff changeset	60
a189c6274c7a type constraints and sort intersection haftmann parents: 22835 diff changeset	61	(* sorts as intersections *)
55038 f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	62
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	63	syntax (xsymbols output)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	64	"_topsort" :: "sort" ("\<top>" 1000)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	65	"_sort" :: "classes => sort" ("'(_')" 1000)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	66	"_classes" :: "id => classes => classes" ("_ \<inter> _" 1000)
f2179be64805 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); wenzelm parents: 42297 diff changeset	67	"_classes" :: "longid => classes => classes" ("_ \<inter> _" 1000)
15469 f5d22f504ab9 new nipkow parents: diff changeset	68
15476 b8cb20cc0c0b fixed bugs nipkow parents: 15469 diff changeset	69	end
b8cb20cc0c0b fixed bugs nipkow parents: 15469 diff changeset	70	(>)

author	paulson <lp15@cam.ac.uk>
	Fri, 20 Mar 2015 16:11:28 +0000
changeset 59765	26d1c71784f1
parent 56245	84fc7dfa3cd4
child 61143	5f898411ce87
permissions	-rw-r--r--