# HG changeset patch
# User wenzelm
# Date 938616323 -7200
# Node ID c89ba43d9df057cabda88d67e255d7b6b2f6161f
# Parent  2d3445be4e9154cc974f9e05db1febb7101565db
bind_thm ("case_split", case_split_thm);

diff -r 2d3445be4e91 -r c89ba43d9df0 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Wed Sep 29 16:45:04 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Sep 29 16:45:23 1999 +0200
@@ -422,6 +422,8 @@
   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
                   etac p2 1, etac p1 1]);
 
+bind_thm ("case_split", case_split_thm);
+
 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;