eliminated obsolete case_split_thm -- use case_split;
added case_split_tac (works without context);
setup for induct_tacs.ML;
(* Title: HOL/Main.thy
ID: $Id$
*)
header {* Main HOL *}
theory Main
imports Map
begin
ML {* val HOL_proofs = ! Proofterm.proofs *}
ML {* path_add "~~/src/HOL/Library" *}
end