src/HOL/HOL.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10433 6c5659d461dd
child 11451 8abfb4f7bd02
permissions -rw-r--r--
improved theory reference in comment
wenzelm@10011
     1
(*  Title:      HOL/HOL.ML
wenzelm@10011
     2
    ID:         $Id$
wenzelm@10011
     3
*)
wenzelm@10011
     4
wenzelm@7357
     5
structure HOL =
wenzelm@7357
     6
struct
wenzelm@7357
     7
  val thy = the_context ();
wenzelm@7357
     8
  val plusI = plusI;
wenzelm@7357
     9
  val minusI = minusI;
wenzelm@7357
    10
  val timesI = timesI;
wenzelm@7357
    11
  val eq_reflection = eq_reflection;
wenzelm@7357
    12
  val refl = refl;
wenzelm@7357
    13
  val subst = subst;
wenzelm@7357
    14
  val ext = ext;
paulson@9970
    15
  val someI = someI;
wenzelm@7357
    16
  val impI = impI;
wenzelm@7357
    17
  val mp = mp;
wenzelm@7357
    18
  val True_def = True_def;
wenzelm@7357
    19
  val All_def = All_def;
wenzelm@7357
    20
  val Ex_def = Ex_def;
wenzelm@7357
    21
  val False_def = False_def;
wenzelm@7357
    22
  val not_def = not_def;
wenzelm@7357
    23
  val and_def = and_def;
wenzelm@7357
    24
  val or_def = or_def;
wenzelm@7357
    25
  val Ex1_def = Ex1_def;
wenzelm@7357
    26
  val iff = iff;
wenzelm@7357
    27
  val True_or_False = True_or_False;
wenzelm@7357
    28
  val Let_def = Let_def;
wenzelm@7357
    29
  val if_def = if_def;
wenzelm@7357
    30
  val arbitrary_def = arbitrary_def;
wenzelm@3621
    31
end;
wenzelm@5888
    32
wenzelm@10062
    33
AddXIs [equal_intr_rule, disjI1, disjI2, ext];
wenzelm@10273
    34
AddXEs [ex1_implies_ex, someI_ex, sym];
wenzelm@7529
    35
wenzelm@7357
    36
open HOL;