Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed case_split thm binding;
authorwenzelm
Tue, 22 Feb 2000 21:39:38 +0100
changeset 8276 2647b7fa6508
parent 8275 32387a2c7749
child 8277 493707fcd8a6
removed case_split thm binding;
src/HOL/HOL_lemmas.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL_lemmas.ML	Tue Feb 22 21:39:01 2000 +0100
+++ b/src/HOL/HOL_lemmas.ML	Tue Feb 22 21:39:38 2000 +0100
@@ -422,8 +422,6 @@
   (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;
isabelle