author  haftmann 
Thu, 15 Jan 2009 14:52:24 +0100  
changeset 29493  ddcbd5e4041d 
parent 27688  397de75836a1 
child 30304  d8e4cd2ac2a1 
permissions  rwrr 
15469  1 
(* Title: HOL/Library/LaTeXsugar.thy 
2 
Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer 

3 
Copyright 2005 NICTA and TUM 

4 
*) 

5 

6 
(*<*) 

7 
theory LaTeXsugar 

27487  8 
imports Plain "~~/src/HOL/List" 
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 
(* should become standard syntax once xsymbols supports it *) 
24 
syntax (latex) 

25 
nexists :: "('a => bool) => bool" (binder "\<nexists>" 10) 

26 
translations 

27 
"\<nexists>x. P" <= "\<not>(\<exists>x. P)" 

28 

15469  29 
(* SETS *) 
30 

31 
(* empty set *) 

27688  32 
notation (latex) 
33 
"{}" ("\<emptyset>") 

15469  34 

35 
(* insert *) 

36 
translations 

37 
"{x} \<union> A" <= "insert x A" 

15690  38 
"{x,y}" <= "{x} \<union> {y}" 
15469  39 
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)" 
27688  40 
"{x}" <= "{x} \<union> \<emptyset>" 
15469  41 

42 
(* set comprehension *) 

43 
syntax (latex output) 

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

45 
translations 

46 
"_Collect p P" <= "{p. P}" 

15690  47 
"_Collect p P" <= "{pxs. P}" 
15469  48 

49 
(* LISTS *) 

50 

51 
(* Cons *) 

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

55 
(* length *) 

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

59 
(* nth *) 

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

63 
(* DUMMY *) 

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

65 

66 
(* THEOREMS *) 

67 
syntax (Rule output) 

68 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 

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

70 

71 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

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

73 

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

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

76 

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

78 

22328
cc403d881873
added printmode Axiom to print theorems without premises with a rule on top.
schirmer
parents:
21210
diff
changeset

79 
syntax (Axiom output) 
cc403d881873
added printmode Axiom to print theorems without premises with a rule on top.
schirmer
parents:
21210
diff
changeset

80 
"Trueprop" :: "bool \<Rightarrow> prop" 
cc403d881873
added printmode Axiom to print theorems without premises with a rule on top.
schirmer
parents:
21210
diff
changeset

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

82 

15469  83 
syntax (IfThen output) 
84 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 

25467  85 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  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 

91 
syntax (IfThenNoBox output) 

92 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 

25467  93 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  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 

99 
end 

100 
(*>*) 