src/Doc/ProgProve/LaTeXsugar.thy
changeset 56245 84fc7dfa3cd4
parent 56002 2028467b4df4
equal deleted inserted replaced
56244:3298b7a2795a 56245:84fc7dfa3cd4
    11 (* DUMMY *)
    11 (* DUMMY *)
    12 consts DUMMY :: 'a ("\<^raw:\_>")
    12 consts DUMMY :: 'a ("\<^raw:\_>")
    13 
    13 
    14 (* THEOREMS *)
    14 (* THEOREMS *)
    15 notation (Rule output)
    15 notation (Rule output)
    16   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    16   Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    17 
    17 
    18 syntax (Rule output)
    18 syntax (Rule output)
    19   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    19   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    20   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    20   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    21 
    21 
    26 
    26 
    27 notation (Axiom output)
    27 notation (Axiom output)
    28   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    28   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    29 
    29 
    30 notation (IfThen output)
    30 notation (IfThen output)
    31   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    31   Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    32 syntax (IfThen output)
    32 syntax (IfThen output)
    33   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    33   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    34   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    34   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    35   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    35   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    36   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    36   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    37 
    37 
    38 notation (IfThenNoBox output)
    38 notation (IfThenNoBox output)
    39   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    39   Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    40 syntax (IfThenNoBox output)
    40 syntax (IfThenNoBox output)
    41   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    41   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    42   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    42   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    43   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    43   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    44   "_asm" :: "prop \<Rightarrow> asms" ("_")
    44   "_asm" :: "prop \<Rightarrow> asms" ("_")