# HG changeset patch
# User wenzelm
# Date 936213917 -7200
# Node ID e5a5d59dd51334d8f0360976a2d3c7eee4262f70
# Parent  e0be36ee7ab9d6c7b6650b45829979d1d2af79cf
bind_thm "case";

diff -r e0be36ee7ab9 -r e5a5d59dd513 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Wed Sep 01 21:24:50 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Sep 01 21:25:17 1999 +0200
@@ -412,6 +412,7 @@
                   etac p2 1, etac p1 1]);
 
 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+bind_thm ("case", case_split_thm);
 
 
 (** Standard abbreviations **)