src/HOL/HOL.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 7529 fa534e4f7e49
child 9396 a1b31d61f8e1
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     2
structure HOL =
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     3
struct
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     4
  val thy = the_context ();
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     5
  val plusI = plusI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     6
  val minusI = minusI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     7
  val timesI = timesI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     8
  val powerI = powerI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     9
  val eq_reflection = eq_reflection;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    10
  val refl = refl;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    11
  val subst = subst;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    12
  val ext = ext;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    13
  val selectI = selectI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    14
  val impI = impI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    15
  val mp = mp;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    16
  val True_def = True_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    17
  val All_def = All_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    18
  val Ex_def = Ex_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    19
  val False_def = False_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    20
  val not_def = not_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    21
  val and_def = and_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    22
  val or_def = or_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    23
  val Ex1_def = Ex1_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    24
  val iff = iff;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    25
  val True_or_False = True_or_False;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    26
  val Let_def = Let_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    27
  val if_def = if_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    28
  val arbitrary_def = arbitrary_def;
3621
d3e248853428 tuned comments;
wenzelm
parents: 3615
diff changeset
    29
end;
5888
d8e51792ca85 attrib_setup: rulify;
wenzelm
parents: 5809
diff changeset
    30
7529
fa534e4f7e49 AddXIs [disjI1, disjI2];
wenzelm
parents: 7357
diff changeset
    31
AddXIs [disjI1, disjI2];
fa534e4f7e49 AddXIs [disjI1, disjI2];
wenzelm
parents: 7357
diff changeset
    32
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    33
open HOL;