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.
reintroduced metisFT in example
authorblanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 43202 6ce09f69657c
parent 43201 0c9bf1a8e0d8
child 43203 6c8170f8849e
reintroduced metisFT in example
src/HOL/Metis_Examples/Proxies.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -66,7 +66,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metisX id_apply)
+by (metisFT id_apply)
 
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -127,7 +127,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] ()
 sledgehammer [type_sys = mangled_preds?, expect = some] ()
 sledgehammer [type_sys = mangled_preds, expect = some] ()
-by metisX
+by metisFT
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
isabelle