author  wenzelm 
Mon, 23 May 2016 21:30:30 +0200  
changeset 63120  629a4c5e953e 
parent 62522  d32c23d29968 
child 63414  beb987127d0f 
permissions  rwrr 
15469  1 
(* Title: HOL/Library/LaTeXsugar.thy 
55077  2 
Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer 
15469  3 
Copyright 2005 NICTA and TUM 
4 
*) 

5 

6 
(*<*) 

7 
theory LaTeXsugar 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30304
diff
changeset

8 
imports Main 
15469  9 
begin 
10 

11 
(* LOGIC *) 

21210  12 
notation (latex output) 
19674  13 
If ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10) 
14 

15469  15 
syntax (latex output) 
16 

17 
"_Let" :: "[letbinds, 'a] => 'a" 

18 
("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) 

19 

20 
"_case_syntax":: "['a, cases_syn] => 'b" 

21 
("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) 

22 

16110  23 

15469  24 
(* SETS *) 
25 

26 
(* empty set *) 

27688  27 
notation (latex) 
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
29493
diff
changeset

28 
"Set.empty" ("\<emptyset>") 
15469  29 

30 
(* insert *) 

31 
translations 

31462  32 
"{x} \<union> A" <= "CONST insert x A" 
15690  33 
"{x,y}" <= "{x} \<union> {y}" 
15469  34 
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)" 
27688  35 
"{x}" <= "{x} \<union> \<emptyset>" 
15469  36 

37 
(* set comprehension *) 

38 
syntax (latex output) 

39 
"_Collect" :: "pttrn => bool => 'a set" ("(1{_  _})") 

41757  40 
"_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _  _})") 
15469  41 
translations 
42 
"_Collect p P" <= "{p. P}" 

15690  43 
"_Collect p P" <= "{pxs. P}" 
41757  44 
"_CollectIn p A P" <= "{p : A. P}" 
15469  45 

56977  46 
(* card *) 
47 
notation (latex output) 

48 
card ("_") 

49 

15469  50 
(* LISTS *) 
51 

52 
(* Cons *) 

21210  53 
notation (latex) 
56977  54 
Cons ("_ \<cdot>/ _" [66,65] 65) 
15469  55 

56 
(* length *) 

21210  57 
notation (latex output) 
19674  58 
length ("_") 
15469  59 

60 
(* nth *) 

21210  61 
notation (latex output) 
19674  62 
nth ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000) 
15469  63 

64 
(* DUMMY *) 

65 
consts DUMMY :: 'a ("\<^raw:\_>") 

66 

67 
(* THEOREMS *) 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

68 
notation (Rule output) 
56245  69 
Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") 
35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

70 

15469  71 
syntax (Rule output) 
72 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

73 
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") 

74 

75 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

76 
("\<^raw:\mbox{>_\<^raw:}\\>/ _") 

77 

78 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 

79 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

80 
notation (Axiom output) 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

81 
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") 
22328
cc403d881873
added printmode Axiom to print theorems without premises with a rule on top.
schirmer
parents:
21210
diff
changeset

82 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

83 
notation (IfThen output) 
56245  84 
Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  85 
syntax (IfThen output) 
86 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

25467  87 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
88 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") 

15469  89 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 
90 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

91 
notation (IfThenNoBox output) 
56245  92 
Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  93 
syntax (IfThenNoBox output) 
94 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

25467  95 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
96 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") 

15469  97 
"_asm" :: "prop \<Rightarrow> asms" ("_") 
98 

60500  99 
setup\<open> 
49628  100 
let 
101 
fun pretty ctxt c = 

56002  102 
let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c 
49628  103 
in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", 
104 
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] 

105 
end 

106 
in 

107 
Thy_Output.antiquotation @{binding "const_typ"} 

63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62522
diff
changeset

108 
(Scan.lift Args.embedded_inner_syntax) 
49628  109 
(fn {source = src, context = ctxt, ...} => fn arg => 
110 
Thy_Output.output ctxt 

111 
(Thy_Output.maybe_pretty_source pretty ctxt src [arg])) 

112 
end; 

60500  113 
\<close> 
49628  114 

15469  115 
end 
55077  116 
(*>*) 