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 36768 46be86127972
parent 36692 54b64d4ad524
child 36936 c52d1c130898 
--- a/src/HOL/HOL.thy	Sun May 09 18:09:30 2010 +0200
+++ b/src/HOL/HOL.thy	Sun May 09 19:15:21 2010 +0200
@@ -1869,7 +1869,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?eq"
isabelle