diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Oct 11 10:49:36 2006 +0200
+++ b/src/HOL/HOL.ML	Wed Oct 11 14:51:24 2006 +0200
@@ -1,6 +1,24 @@
 (* legacy ML bindings *)
 
+val HOL_cs = HOL.claset;
+val HOL_basic_ss = HOL.simpset_basic;
+val HOL_ss = HOL.simpset;
+val HOL_css = (HOL.claset, HOL.simpset);
+val hol_simplify = HOL.simplify;
+
+val split_tac        = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac    = Splitter.split_asm_tac;
+val op addsplits     = Splitter.addsplits;
+val op delsplits     = Splitter.delsplits;
+val Addsplits        = Splitter.Addsplits;
+val Delsplits        = Splitter.Delsplits;
+
 open HOL;
+val claset = Classical.claset;
+val simpset = Simplifier.simpset;
+val simplify = Simplifier.simplify;
+open Clasimp;
 
 val ext = thm "ext"
 val True_def = thm "True_def"