src/HOL/Plain.thy
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 47108 2a1953f0d20d
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27368
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     1
header {* Plain HOL *}
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     2
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     3
theory Plain
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46691
diff changeset
     4
imports Datatype FunDef Extraction Metis Num
27368
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     5
begin
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     6
29304
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 27368
diff changeset
     7
text {*
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 27368
diff changeset
     8
  Plain bootstrap of fundamental HOL tools and packages; does not
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 27368
diff changeset
     9
  include @{text Hilbert_Choice}.
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 27368
diff changeset
    10
*}
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 27368
diff changeset
    11
46691
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    12
no_notation
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    13
  bot ("\<bottom>") and
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    14
  top ("\<top>") and
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    15
  inf (infixl "\<sqinter>" 70) and
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    16
  sup (infixl "\<squnion>" 65) and
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    17
  Inf ("\<Sqinter>_" [900] 900) and
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    18
  Sup ("\<Squnion>_" [900] 900)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    19
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    20
no_syntax (xsymbols)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    21
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    22
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    23
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    24
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure
haftmann
parents: 41886
diff changeset
    25
27368
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
    26
end