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/Examples/Iff_Oracle.thy
changeset 77867 686a7d71ed7b
parent 77824 e3fe192fa4a8 
--- a/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 18 11:58:12 2023 +0200
+++ b/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 18 12:04:41 2023 +0200
@@ -36,8 +36,7 @@
 ML \<open>iff_oracle (\<^theory>, 10)\<close>
 
 ML \<open>
-  \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) =
-    [\<^oracle_name>\<open>iff_oracle\<close>]);
+  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
 \<close>
 
 text \<open>These oracle calls had better fail.\<close>
isabelle