src/FOL/cladata.ML

replaced File.check by specific File.check_file, File.check_dir;
clarified File.full_path -- include parts of former Thy_Load.get_file;
simplified Thy_Load.check_file -- do not read/digest yet;
merged Thy_Load.check_thy/deps_thy -- always read text and parse header;
clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator;
Thy_Info.check_deps etc.: File.read exactly once;

(*  Title:      FOL/cladata.ML
    Author:     Tobias Nipkow
    Copyright   1996  University of Cambridge

Setting up the classical reasoner.
*)

(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data = 
struct
  val imp_elim  = @{thm imp_elim}
  val not_elim  = @{thm notE}
  val swap      = @{thm swap}
  val classical = @{thm classical}
  val sizef     = size_of_thm
  val hyp_subst_tacs=[hyp_subst_tac]
end;

structure Cla = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;

ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");


(*Propositional rules*)
val prop_cs = empty_cs
  addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
    @{thm notI}, @{thm iffI}]
  addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];

(*Quantifier rules*)
val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
                     addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];