src/HOL/Main.thy
author blanchet
Mon, 20 Jan 2014 18:24:56 +0100
changeset 55069 b3e44be90122
parent 55067 a452de24a877
child 55078 558c9ceabaa1
permissions -rw-r--r--
moved hide_const from BNF to Main
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     1
header {* Main HOL *}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     2
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     3
theory Main
55062
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55058
diff changeset
     4
imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     5
begin
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
     6
29304
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     7
text {*
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     8
  Classical Higher-order Logic -- only ``Main'', excluding real and
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     9
  complex numbers etc.
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
    10
*}
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
    11
27367
a75d71c73362 added dummy citiation
haftmann
parents: 26729
diff changeset
    12
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
25964
080f89d89990 consistent interacitve bootstrap of HOL-Main
haftmann
parents: 25223
diff changeset
    13
55069
b3e44be90122 moved hide_const from BNF to Main
blanchet
parents: 55067
diff changeset
    14
hide_const (open)
b3e44be90122 moved hide_const from BNF to Main
blanchet
parents: 55067
diff changeset
    15
  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
b3e44be90122 moved hide_const from BNF to Main
blanchet
parents: 55067
diff changeset
    16
  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
b3e44be90122 moved hide_const from BNF to Main
blanchet
parents: 55067
diff changeset
    17
  prefCl PrefCl Succ Shift shift proj
b3e44be90122 moved hide_const from BNF to Main
blanchet
parents: 55067
diff changeset
    18
51112
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    19
no_notation
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    20
  bot ("\<bottom>") and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    21
  top ("\<top>") and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    22
  inf (infixl "\<sqinter>" 70) and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    23
  sup (infixl "\<squnion>" 65) and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    24
  Inf ("\<Sqinter>_" [900] 900) and
55057
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    25
  Sup ("\<Squnion>_" [900] 900) and
55065
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    26
  ordLeq2 (infix "<=o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    27
  ordLeq3 (infix "\<le>o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    28
  ordLess2 (infix "<o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    29
  ordIso2 (infix "=o" 50) and
55057
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    30
  csum (infixr "+c" 65) and
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    31
  cprod (infixr "*c" 80) and
55067
a452de24a877 tuned names
blanchet
parents: 55066
diff changeset
    32
  cexp (infixr "^c" 90)
51112
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    33
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    34
no_syntax (xsymbols)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    35
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    36
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    37
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    38
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    39
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    40
end