src/HOL/Main.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 66954 0230af0f3c59
child 67385 deb9b0283259
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@65553
     1
section \<open>Main HOL\<close>
wenzelm@65553
     2
wenzelm@65553
     3
text \<open>
wenzelm@65553
     4
  Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@65553
     5
  complex numbers etc.
wenzelm@65553
     6
\<close>
wenzelm@65553
     7
wenzelm@65553
     8
theory Main
haftmann@66817
     9
  imports
haftmann@66817
    10
    Predicate_Compile
haftmann@66817
    11
    Quickcheck_Narrowing 
haftmann@66817
    12
    Extraction
haftmann@66817
    13
    Nunchaku
haftmann@66817
    14
    BNF_Greatest_Fixpoint Filter
haftmann@66817
    15
    Conditionally_Complete_Lattices
haftmann@66817
    16
    Binomial
haftmann@66817
    17
    GCD
wenzelm@65553
    18
begin
wenzelm@65553
    19
wenzelm@65814
    20
text \<open>
wenzelm@65814
    21
  Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@65814
    22
  complex numbers etc.
wenzelm@65814
    23
\<close>
wenzelm@65814
    24
wenzelm@65814
    25
no_notation
wenzelm@65814
    26
  bot ("\<bottom>") and
wenzelm@65814
    27
  top ("\<top>") and
wenzelm@65814
    28
  inf (infixl "\<sqinter>" 70) and
wenzelm@65814
    29
  sup (infixl "\<squnion>" 65) and
wenzelm@65814
    30
  Inf ("\<Sqinter>_" [900] 900) and
wenzelm@65814
    31
  Sup ("\<Squnion>_" [900] 900) and
wenzelm@65814
    32
  ordLeq2 (infix "<=o" 50) and
wenzelm@65814
    33
  ordLeq3 (infix "\<le>o" 50) and
wenzelm@65814
    34
  ordLess2 (infix "<o" 50) and
wenzelm@65814
    35
  ordIso2 (infix "=o" 50) and
wenzelm@65814
    36
  card_of ("|_|") and
wenzelm@65814
    37
  csum (infixr "+c" 65) and
wenzelm@65814
    38
  cprod (infixr "*c" 80) and
wenzelm@65814
    39
  cexp (infixr "^c" 90) and
wenzelm@65814
    40
  convol ("\<langle>(_,/ _)\<rangle>")
wenzelm@65814
    41
wenzelm@65814
    42
hide_const (open)
wenzelm@65814
    43
  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
wenzelm@65814
    44
  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
wenzelm@65814
    45
  shift proj id_bnf
wenzelm@65814
    46
wenzelm@65814
    47
hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
wenzelm@65814
    48
wenzelm@65814
    49
no_syntax
wenzelm@65814
    50
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
wenzelm@65814
    51
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
wenzelm@65814
    52
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
wenzelm@65814
    53
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
wenzelm@65814
    54
wenzelm@65553
    55
end