(*  Title:      HOL/HOL.ML
    ID:         $Id: HOL_BASIC.ML,v 1.2 2003/02/28 13:30:46 smaus Exp $
*)

(*modified by Jan Smaus, 13.12.01.
Purpose: create a minimal HOL environment where many things are missing
so that they can be given as exercises*)

structure HOL_BASIC =
struct
  val thy = the_context ();
  val eq_reflection = thm"eq_reflection";
  val refl = thm "refl";
  val subst = thm "subst";
  val ext =  thm"ext";
  val someI = thm "someI";
  val impI = thm "impI";
  val mp = thm "mp";
  val True_def = thm "True_def";
  val All_def = thm "All_def";
  val Ex_def = thm "Ex_def";
  val False_def = thm "False_def";
  val not_def = thm "not_def";
  val and_def = thm "and_def";
  val or_def = thm "or_def";
  val Ex1_def = thm "Ex1_def";
  val iff = thm "iff";
  val True_or_False = thm "True_or_False";
  val Let_def = thm "Let_def";
  val if_def = thm "if_def";
  val arbitrary_def = thm "arbitrary_def";
end;

open HOL_BASIC;