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.
use more informative Thm.proof_body_of for oracle demo;
authorwenzelm
Wed, 25 Mar 2009 17:23:44 +0100
changeset 30719 21c20c7d1932
parent 30718 15041c7e51e4
child 30720 6d8dcfb264dc
use more informative Thm.proof_body_of for oracle demo;
src/FOL/ex/Iff_Oracle.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/ex/Iff_Oracle.thy	Wed Mar 25 16:54:49 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy	Wed Mar 25 17:23:44 2009 +0100
@@ -34,7 +34,7 @@
 
 ML {* iff_oracle (@{theory}, 2) *}
 ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
+ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
 
 text {* These oracle calls had better fail. *}
isabelle