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.
update example
authorblanchet
Fri, 20 May 2011 18:12:12 +0200
changeset 42896 d96e53d0c638
parent 42895 c8d9bce88f89
child 42897 6bc8a6dcb3e0
child 42901 e35cf2b25f48
update example
src/HOL/Metis_Examples/HO_Reas.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 18:01:46 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 18:12:12 2011 +0200
@@ -56,7 +56,7 @@
 
 lemma "id (op =) x x"
 sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
isabelle