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.
normalization uses refl now
authornipkow
Fri, 30 Jun 2006 18:26:22 +0200
changeset 19970 d6e238c46d1b
parent 19969 c72e2110c026
child 19971 ddf69abaffa8
normalization uses refl now
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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