47269

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 
(*>*) 