src/HOL/HOL.ML
author wenzelm
Thu, 19 Oct 2000 21:20:53 +0200
changeset 10273 59570adf2d3c
parent 10182 5413bcce1482
child 10433 6c5659d461dd
permissions -rw-r--r--
declare sym [elim?] in HOL.ML instead of Calculation.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10011
ed5262aee27f AddXIs [ext];
wenzelm
parents: 9970
diff changeset
     1
(*  Title:      HOL/HOL.ML
ed5262aee27f AddXIs [ext];
wenzelm
parents: 9970
diff changeset
     2
    ID:         $Id$
ed5262aee27f AddXIs [ext];
wenzelm
parents: 9970
diff changeset
     3
*)
ed5262aee27f AddXIs [ext];
wenzelm
parents: 9970
diff changeset
     4
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     5
structure HOL =
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     6
struct
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     7
  val thy = the_context ();
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     8
  val plusI = plusI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
     9
  val minusI = minusI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    10
  val timesI = timesI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    11
  val powerI = powerI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    12
  val eq_reflection = eq_reflection;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    13
  val refl = refl;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    14
  val subst = subst;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    15
  val ext = ext;
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 9396
diff changeset
    16
  val someI = someI;
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    17
  val impI = impI;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    18
  val mp = mp;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    19
  val True_def = True_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    20
  val All_def = All_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    21
  val Ex_def = Ex_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    22
  val False_def = False_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    23
  val not_def = not_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    24
  val and_def = and_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    25
  val or_def = or_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    26
  val Ex1_def = Ex1_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    27
  val iff = iff;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    28
  val True_or_False = True_or_False;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    29
  val Let_def = Let_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    30
  val if_def = if_def;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    31
  val arbitrary_def = arbitrary_def;
3621
d3e248853428 tuned comments;
wenzelm
parents: 3615
diff changeset
    32
end;
5888
d8e51792ca85 attrib_setup: rulify;
wenzelm
parents: 5809
diff changeset
    33
10062
3b819da9c71a AddXIs [equal_intr_rule];
wenzelm
parents: 10011
diff changeset
    34
AddXIs [equal_intr_rule, disjI1, disjI2, ext];
10273
59570adf2d3c declare sym [elim?] in HOL.ML instead of Calculation.thy;
wenzelm
parents: 10182
diff changeset
    35
AddXEs [ex1_implies_ex, someI_ex, sym];
7529
fa534e4f7e49 AddXIs [disjI1, disjI2];
wenzelm
parents: 7357
diff changeset
    36
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 7030
diff changeset
    37
open HOL;