equal
deleted
inserted
replaced
34 |
34 |
35 ML \<open>iff_oracle (\<^theory>, 2)\<close> |
35 ML \<open>iff_oracle (\<^theory>, 2)\<close> |
36 ML \<open>iff_oracle (\<^theory>, 10)\<close> |
36 ML \<open>iff_oracle (\<^theory>, 10)\<close> |
37 |
37 |
38 ML \<open> |
38 ML \<open> |
39 Thm.peek_status (iff_oracle (\<^theory>, 10)); |
39 \<^assert> (map #1 (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]); |
40 \<^assert> (#oracle it); |
|
41 \<close> |
40 \<close> |
42 |
41 |
43 text \<open>These oracle calls had better fail.\<close> |
42 text \<open>These oracle calls had better fail.\<close> |
44 |
43 |
45 ML \<open> |
44 ML \<open> |