# HG changeset patch
# User wenzelm
# Date 1165363976 -3600
# Node ID 8a6bf9d7c7511c021c24c86585adc249d91e419c
# Parent  a664ba87b3aa283c3fa7837857ff1b59796769fa
simplified ML bindings -- moved to HOL.thy;
removed confusing simpset_basic/simplify;

diff -r a664ba87b3aa -r 8a6bf9d7c751 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Dec 06 01:12:51 2006 +0100
+++ b/src/HOL/simpdata.ML	Wed Dec 06 01:12:56 2006 +0100
@@ -163,19 +163,29 @@
 
 structure Splitter = SplitterFun(SplitterData);
 
+val split_tac        = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+
+val op addsplits     = Splitter.addsplits;
+val op delsplits     = Splitter.delsplits;
+val Addsplits        = Splitter.Addsplits;
+val Delsplits        = Splitter.Delsplits;
+
+
 (* integration of simplifier with classical reasoner *)
 
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
+  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
+open Clasimp;
 
 val mksimps_pairs =
   [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
    ("All", [thm "spec"]), ("True", []), ("False", []),
    ("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])];
 
-val simpset_basic =
+val HOL_basic_ss =
   Simplifier.theory_context (the_context ()) empty_ss
     setsubgoaler asm_simp_tac
     setSSolver safe_solver
@@ -184,10 +194,10 @@
     setmkeqTrue mk_eq_True
     setmkcong mk_meta_cong;
 
-fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
+fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
 
 fun unfold_tac ths =
-  let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
+  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 
@@ -338,7 +348,7 @@
     "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
 
 
-val simpset_simprocs = simpset_basic
+val simpset_simprocs = HOL_basic_ss
   addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
 
 end;