|
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 |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 (* DUMMY *) |
|
12 consts DUMMY :: 'a ("\<^raw:\_>") |
|
13 |
|
14 (* THEOREMS *) |
|
15 notation (Rule output) |
|
16 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
17 |
|
18 syntax (Rule output) |
|
19 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
20 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
21 |
|
22 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
23 ("\<^raw:\mbox{>_\<^raw:}\\>/ _") |
|
24 |
|
25 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
26 |
|
27 notation (Axiom output) |
|
28 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
|
29 |
|
30 notation (IfThen output) |
|
31 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
32 syntax (IfThen output) |
|
33 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
34 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
35 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
36 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
37 |
|
38 notation (IfThenNoBox output) |
|
39 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
40 syntax (IfThenNoBox output) |
|
41 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
42 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
43 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
44 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
45 |
|
46 end |
|
47 (*>*) |