1 (* Title: HOL/Library/LaTeXsugar.thy |
|
2 Author: Gerwin Klein, 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 Pure.imp ("\<^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 Pure.imp ("\<^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 Pure.imp ("\<^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 setup{* |
|
47 let |
|
48 fun pretty ctxt c = |
|
49 let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c |
|
50 in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", |
|
51 Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] |
|
52 end |
|
53 in |
|
54 Thy_Output.antiquotation @{binding "const_typ"} |
|
55 (Scan.lift Args.name_inner_syntax) |
|
56 (fn {source = src, context = ctxt, ...} => fn arg => |
|
57 Thy_Output.output ctxt |
|
58 (Thy_Output.maybe_pretty_source pretty ctxt src [arg])) |
|
59 end; |
|
60 *} |
|
61 |
|
62 end |
|
63 (*>*) |
|