src/HOL/HOL.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15524 2ef571f80a55
child 17274 746bb4c56800
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
wenzelm@12999
     1
(* legacy ML bindings *)
wenzelm@11749
     2
berghofe@13638
     3
val choice_eq = thm "choice_eq";
wenzelm@12999
     4
wenzelm@12999
     5
structure HOL =
wenzelm@12999
     6
struct
wenzelm@12999
     7
  val thy = the_context ();
wenzelm@12999
     8
  val plusI = plusI;
wenzelm@12999
     9
  val minusI = minusI;
wenzelm@12999
    10
  val timesI = timesI;
wenzelm@12999
    11
  val eq_reflection = eq_reflection;
wenzelm@12999
    12
  val refl = refl;
wenzelm@12999
    13
  val subst = subst;
wenzelm@12999
    14
  val ext = ext;
wenzelm@12999
    15
  val impI = impI;
wenzelm@12999
    16
  val mp = mp;
wenzelm@12999
    17
  val True_def = True_def;
wenzelm@12999
    18
  val All_def = All_def;
wenzelm@12999
    19
  val Ex_def = Ex_def;
wenzelm@12999
    20
  val False_def = False_def;
wenzelm@12999
    21
  val not_def = not_def;
wenzelm@12999
    22
  val and_def = and_def;
wenzelm@12999
    23
  val or_def = or_def;
wenzelm@12999
    24
  val Ex1_def = Ex1_def;
wenzelm@12999
    25
  val iff = iff;
wenzelm@12999
    26
  val True_or_False = True_or_False;
wenzelm@12999
    27
  val Let_def = Let_def;
wenzelm@12999
    28
  val if_def = if_def;
wenzelm@12999
    29
end;
wenzelm@12999
    30
wenzelm@12999
    31
open HOL;