src/Doc/ProgProve/LaTeXsugar.thy
author nipkow
Fri, 28 Sep 2012 08:59:54 +0200
changeset 49629 99700c4e0b33
parent 48985 5386df44a037
child 55111 5792f5106c40
permissions -rw-r--r--
second usage of const_typ
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/LaTeXsugar.thy
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
    Copyright   2005 NICTA and TUM
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
theory LaTeXsugar
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
imports Main
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
begin
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
(* DUMMY *)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
consts DUMMY :: 'a ("\<^raw:\_>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
(* THEOREMS *)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
notation (Rule output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
syntax (Rule output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
notation (Axiom output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
notation (IfThen output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
syntax (IfThen output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
notation (IfThenNoBox output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    40
syntax (IfThenNoBox output)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    41
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    42
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
  "_asm" :: "prop \<Rightarrow> asms" ("_")
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    45
49629
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    46
setup{*
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    47
  let
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    48
    fun pretty ctxt c =
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    49
      let val tc = Proof_Context.read_const_proper ctxt false c
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    50
      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    51
            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    52
      end
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    53
  in
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    54
    Thy_Output.antiquotation @{binding "const_typ"}
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    55
     (Scan.lift Args.name_source)
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    56
       (fn {source = src, context = ctxt, ...} => fn arg =>
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    57
          Thy_Output.output ctxt
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    58
            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    59
  end;
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    60
*}
99700c4e0b33 second usage of const_typ
nipkow
parents: 48985
diff changeset
    61
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    62
end
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    63
(*>*)