src/HOL/Main.thy
author wenzelm
Sat, 09 Apr 2016 12:36:25 +0200
changeset 62921 499a63c30d55
parent 61955 e96292f32c3c
child 63331 247eac9758dd
permissions -rw-r--r--
old;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60036
diff changeset
     1
section \<open>Main HOL\<close>
12024
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
60036
218fcc645d22 move filters to their own theory
hoelzl
parents: 58916
diff changeset
     4
imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60036
diff changeset
     7
text \<open>
29304
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.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60036
diff changeset
    10
\<close>
29304
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
    11
51112
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    12
no_notation
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    13
  bot ("\<bottom>") and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    14
  top ("\<top>") and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    15
  inf (infixl "\<sqinter>" 70) and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    16
  sup (infixl "\<squnion>" 65) and
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    17
  Inf ("\<Sqinter>_" [900] 900) and
55057
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    18
  Sup ("\<Squnion>_" [900] 900) and
55065
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    19
  ordLeq2 (infix "<=o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    20
  ordLeq3 (infix "\<le>o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    21
  ordLess2 (infix "<o" 50) and
6d0af3c10864 compile
blanchet
parents: 55062
diff changeset
    22
  ordIso2 (infix "=o" 50) and
55078
558c9ceabaa1 deactivate one more cardinal notation
blanchet
parents: 55069
diff changeset
    23
  card_of ("|_|") and
55057
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    24
  csum (infixr "+c" 65) and
6b0fcbeebaba kill notations
blanchet
parents: 55056
diff changeset
    25
  cprod (infixr "*c" 80) and
55086
500ef036117b hide BNF notation
blanchet
parents: 55079
diff changeset
    26
  cexp (infixr "^c" 90) and
57641
dc59f147b27d more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents: 57208
diff changeset
    27
  convol ("\<langle>(_,/ _)\<rangle>")
51112
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    28
55087
252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents: 55086
diff changeset
    29
hide_const (open)
58152
6fe60a9a5bad use 'datatype_new' in 'Main'
blanchet
parents: 58128
diff changeset
    30
  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
6fe60a9a5bad use 'datatype_new' in 'Main'
blanchet
parents: 58128
diff changeset
    31
  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
58353
c9f374b64d99 tuned fact visibility
blanchet
parents: 58352
diff changeset
    32
  shift proj id_bnf
c9f374b64d99 tuned fact visibility
blanchet
parents: 58352
diff changeset
    33
c9f374b64d99 tuned fact visibility
blanchet
parents: 58352
diff changeset
    34
hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
55087
252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents: 55086
diff changeset
    35
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 60758
diff changeset
    36
no_syntax
51112
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    37
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    38
  "_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
    39
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain
haftmann
parents: 46155
diff changeset
    40
  "_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
    41
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    42
end