Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Sum_Type.thy
changeset 55403 677569668824
parent 55393 ce5cebfaedda
child 55414 eab03e9cee8a 
--- a/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -107,7 +107,6 @@
 declare
   old.sum.inject[iff del]
   old.sum.distinct(1)[simp del, induct_simp del]
-  old.sum.cases[simp del]
 
 lemmas induct = old.sum.induct
 lemmas inducts = old.sum.inducts
isabelle