# HG changeset patch
# User oheimb
# Date 849123393 -3600
# Node ID c741309167bf29870f59fdda78d4bda0037b4ce6
# Parent  c7ee913746fdea781e3c892e16a2ead53b9a68f7
moved split_tac

diff -r c7ee913746fd -r c741309167bf src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Nov 27 17:00:25 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 27 20:36:33 1996 +0100
@@ -262,6 +262,17 @@
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
                    (fn _ => [rtac expand_if 1]);
 
+local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
+in
+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;
+
+
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
 
@@ -308,17 +319,6 @@
       addcongs [imp_cong];
 
 
-local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
-in
-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;
-
-
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);