47269

1 
(* Title: HOL/Library/LaTeXsugar.thy

55116

2 
Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer

47269

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)

56245

16 
Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

47269

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)

56245

31 
Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

47269

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)

56245

39 
Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

47269

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 

49629

46 
setup{*


47 
let


48 
fun pretty ctxt c =

56002

49 
let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c

49629

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"}

55111

55 
(Scan.lift Args.name_inner_syntax)

49629

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 

47269

62 
end


63 
(*>*) 