src/HOL/Library/LaTeXsugar.thy
changeset 63935 aa1fe1103ab8
parent 63414 beb987127d0f
child 66527 7ca69030a2af
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Wed Sep 21 22:44:24 2016 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Sep 22 00:12:17 2016 +0200
     1.3 @@ -10,15 +10,15 @@
     1.4  
     1.5  (* LOGIC *)
     1.6  notation (latex output)
     1.7 -  If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
     1.8 +  If  ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)
     1.9  
    1.10  syntax (latex output)
    1.11  
    1.12    "_Let"        :: "[letbinds, 'a] => 'a"
    1.13 -  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    1.14 +  ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
    1.15  
    1.16    "_case_syntax":: "['a, cases_syn] => 'b"
    1.17 -  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    1.18 +  ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
    1.19  
    1.20  
    1.21  (* SETS *)
    1.22 @@ -59,41 +59,41 @@
    1.23  
    1.24  (* nth *)
    1.25  notation (latex output)
    1.26 -  nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    1.27 +  nth  ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
    1.28  
    1.29  (* DUMMY *)
    1.30 -consts DUMMY :: 'a ("\<^raw:\_>")
    1.31 +consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
    1.32  
    1.33  (* THEOREMS *)
    1.34  notation (Rule output)
    1.35 -  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.36 +  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    1.37  
    1.38  syntax (Rule output)
    1.39    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.40 -  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.41 +  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    1.42  
    1.43    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    1.44 -  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    1.45 +  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
    1.46  
    1.47 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.48 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    1.49  
    1.50  notation (Axiom output)
    1.51 -  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    1.52 +  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    1.53  
    1.54  notation (IfThen output)
    1.55 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.56 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    1.57  syntax (IfThen output)
    1.58    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.59 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.60 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    1.61 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.62 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    1.63 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    1.64 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    1.65  
    1.66  notation (IfThenNoBox output)
    1.67 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.68 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    1.69  syntax (IfThenNoBox output)
    1.70    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.71 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.72 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    1.73 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    1.74 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    1.75    "_asm" :: "prop \<Rightarrow> asms" ("_")
    1.76  
    1.77  setup\<open>