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.
more precise tactics
authorhaftmann
Mon, 24 Apr 2006 16:37:37 +0200
changeset 19458 a70f1b0f09cd
parent 19457 b6eb4b4546fa
child 19459 2041d472fc17
more precise tactics
src/HOL/Tools/datatype_codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:07 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:37 2006 +0200
@@ -311,12 +311,12 @@
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   in
-    (TRY o ALLGOALS o resolve_tac) [HOL.eq_reflection]
+    (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
     THEN (
-      (ALLGOALS o resolve_tac) (eqTrueI :: inject)
+      (ALLGOALS o match_tac) (eqTrueI :: inject)
       ORELSE (ALLGOALS o simp_tac) simpset
     )
-    THEN (ALLGOALS o resolve_tac) [HOL.refl, Drule.reflexive_thm]
+    THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
   end;
 
 fun get_datatype_spec_thms thy dtco =
isabelle