removed "case" thm;
authorwenzelm
Tue Sep 21 17:28:02 1999 +0200 (1999-09-21 ago)
changeset 756019c3be2d285c
parent 7559 1d2c099e98f7
child 7561 ff8dbd0589aa
removed "case" thm;
src/HOL/HOL_lemmas.ML
     1.1 --- a/src/HOL/HOL_lemmas.ML	Tue Sep 21 17:26:50 1999 +0200
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Tue Sep 21 17:28:02 1999 +0200
     1.3 @@ -412,7 +412,6 @@
     1.4                    etac p2 1, etac p1 1]);
     1.5  
     1.6  fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
     1.7 -bind_thm ("case", case_split_thm);
     1.8  
     1.9  
    1.10  (** Standard abbreviations **)