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.
Fixed inefficiency in post_definition by adding weak case congruence
authorberghofe
Wed, 01 Oct 2003 11:02:36 +0200
changeset 14217 9f5679e97eac
parent 14216 a15951091d5d
child 14218 db95d1c2f51b
Fixed inefficiency in post_definition by adding weak case congruence rules to simpset.
TFL/tfl.ML file | annotate | diff | comparison | revisions 
--- a/TFL/tfl.ML	Tue Sep 30 17:05:50 2003 +0200
+++ b/TFL/tfl.ML	Wed Oct 01 11:02:36 2003 +0200
@@ -446,7 +446,9 @@
      val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
                            given_pats
      val (case_rewrites,context_congs) = extraction_thms theory
-     val corollaries' = map(rewrite_rule case_rewrites) corollaries
+     val case_ss = HOL_basic_ss addcongs
+       DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
+     val corollaries' = map (Simplifier.simplify case_ss) corollaries
      val extract = R.CONTEXT_REWRITE_RULE
                      (f, [R], cut_apply, meta_tflCongs@context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
isabelle