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/HOL.thy
changeset 19970 d6e238c46d1b
parent 19961 5aa2e37e250c
child 20018 5419a71d0baa 
--- a/src/HOL/HOL.thy	Fri Jun 30 12:22:29 2006 +0200
+++ b/src/HOL/HOL.thy	Fri Jun 30 18:26:22 2006 +0200
@@ -1290,7 +1290,7 @@
   (Drule.goals_conv (equal i) normalization_conv));
 
 val normalization_meth =
-  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN rtac TrueI 1));
+  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI,refl] 1));
 
 in
isabelle