# HG changeset patch
# User berghofe
# Date 831388865 -7200
# Node ID bb326972ede6f72364e73c8be3f85c758a865803
# Parent  445654b6cb950fef90b2b51b38db40a09c7d476a
Added split_inside_tac.

diff -r 445654b6cb95 -r bb326972ede6 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon May 06 15:19:50 1996 +0200
+++ b/src/FOL/simpdata.ML	Mon May 06 15:21:05 1996 +0200
@@ -144,3 +144,10 @@
 in
 fun split_tac splits = mktac (map mk_meta_eq splits)
 end;
+
+local val mktac = mk_case_split_inside_tac meta_iffD
+in
+fun split_inside_tac splits = mktac (map mk_meta_eq splits)
+end;
+
+
diff -r 445654b6cb95 -r bb326972ede6 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon May 06 15:19:50 1996 +0200
+++ b/src/HOL/simpdata.ML	Mon May 06 15:21:05 1996 +0200
@@ -124,6 +124,11 @@
 fun split_tac splits = mktac (map mk_meta_eq splits)
 end;
 
+local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
+in
+fun split_inside_tac splits = mktac (map mk_meta_eq splits)
+end;
+
 
 (* eliminiation of existential quantifiers in assumptions *)