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.
Injectivity / distinctness theorems are now used to simplify induction rules.
authorberghofe
Sun, 10 Jan 2010 18:11:00 +0100
changeset 34911 771830d3bd5e
parent 34910 b23bd3ee4813
child 34912 c04747153bcf
Injectivity / distinctness theorems are now used to simplify induction rules.
src/HOL/Tools/Datatype/datatype_data.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Jan 10 18:09:11 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Jan 10 18:11:00 2010 +0100
@@ -341,7 +341,8 @@
         ((Binding.empty, flat inject), [iff_add]),
         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
           [Classical.safe_elim NONE]),
-        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
+        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
+        ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
         @ named_rules @ unnamed_rules)
     |> snd
     |> add_case_tr' case_names
isabelle