# HG changeset patch
# User wenzelm
# Date 1591646114 -7200
# Node ID bee83c9d330664ada34f06534a98f2a986124669
# Parent  bf085daea304e966a4b3f2dcb280338242dfc40c
clarified sessions;

diff -r bf085daea304 -r bee83c9d3306 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Jun 08 21:38:41 2020 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Jun 08 21:55:14 2020 +0200
@@ -1451,8 +1451,8 @@
   infinitary specification of axioms! Invoking the oracle only works within
   the scope of the resulting theory.
 
-  See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
-  primitive rule as oracle, and turning it into a proof method.
+  See \<^file>\<open>~~/src/HOL/Examples/Iff_Oracle.thy\<close> for a worked example of defining
+  a new primitive rule as oracle, and turning it into a proof method.
 
   \<^descr> \<^theory_text>\<open>thm_oracles thms\<close> displays all oracles used in the internal derivation
   of the given theorems; this covers the full graph of transitive
diff -r bf085daea304 -r bee83c9d3306 src/HOL/Examples/Iff_Oracle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Iff_Oracle.thy	Mon Jun 08 21:55:14 2020 +0200
@@ -0,0 +1,78 @@
+(*  Title:      HOL/Example/Iff_Oracle.thy
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Makarius
+*)
+
+section \<open>Example of Declaring an Oracle\<close>
+
+theory Iff_Oracle
+  imports Main
+begin
+
+subsection \<open>Oracle declaration\<close>
+
+text \<open>
+  This oracle makes tautologies of the form \<^prop>\<open>P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P\<close>.
+  The length is specified by an integer, which is checked to be even
+  and positive.
+\<close>
+
+oracle iff_oracle = \<open>
+  let
+    fun mk_iff 1 = Var (("P", 0), \<^typ>\<open>bool\<close>)
+      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), \<^typ>\<open>bool\<close>), mk_iff (n - 1));
+  in
+    fn (thy, n) =>
+      if n > 0 andalso n mod 2 = 0
+      then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
+      else raise Fail ("iff_oracle: " ^ string_of_int n)
+  end
+\<close>
+
+
+subsection \<open>Oracle as low-level rule\<close>
+
+ML \<open>iff_oracle (\<^theory>, 2)\<close>
+ML \<open>iff_oracle (\<^theory>, 10)\<close>
+
+ML \<open>
+  \<^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>
+
+ML \<open>
+  (iff_oracle (\<^theory>, 5); error "Bad oracle")
+    handle Fail _ => writeln "Oracle failed, as expected"
+\<close>
+
+ML \<open>
+  (iff_oracle (\<^theory>, 1); error "Bad oracle")
+    handle Fail _ => writeln "Oracle failed, as expected"
+\<close>
+
+
+subsection \<open>Oracle as proof method\<close>
+
+method_setup iff =
+  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
+    SIMPLE_METHOD
+      (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
+        handle Fail _ => no_tac))\<close>
+
+
+lemma "A \<longleftrightarrow> A"
+  by (iff 2)
+
+lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
+  by (iff 10)
+
+lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
+  apply (iff 5)?
+  oops
+
+lemma A
+  apply (iff 1)?
+  oops
+
+end
diff -r bf085daea304 -r bee83c9d3306 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jun 08 21:38:41 2020 +0200
+++ b/src/HOL/ROOT	Mon Jun 08 21:55:14 2020 +0200
@@ -26,6 +26,7 @@
     Cantor
     Seq
     "ML"
+    Iff_Oracle
   document_files
     "root.bib"
     "root.tex"
@@ -642,7 +643,6 @@
     Hebrew
     Hex_Bin_Examples
     IArray_Examples
-    Iff_Oracle
     Induction_Schema
     Intuitionistic
     Join_Theory
diff -r bf085daea304 -r bee83c9d3306 src/HOL/ex/Iff_Oracle.thy
--- a/src/HOL/ex/Iff_Oracle.thy	Mon Jun 08 21:38:41 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      HOL/ex/Iff_Oracle.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Makarius
-*)
-
-section \<open>Example of Declaring an Oracle\<close>
-
-theory Iff_Oracle
-imports Main
-begin
-
-subsection \<open>Oracle declaration\<close>
-
-text \<open>
-  This oracle makes tautologies of the form \<^prop>\<open>P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P\<close>.
-  The length is specified by an integer, which is checked to be even
-  and positive.
-\<close>
-
-oracle iff_oracle = \<open>
-  let
-    fun mk_iff 1 = Var (("P", 0), \<^typ>\<open>bool\<close>)
-      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), \<^typ>\<open>bool\<close>), mk_iff (n - 1));
-  in
-    fn (thy, n) =>
-      if n > 0 andalso n mod 2 = 0
-      then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
-      else raise Fail ("iff_oracle: " ^ string_of_int n)
-  end
-\<close>
-
-
-subsection \<open>Oracle as low-level rule\<close>
-
-ML \<open>iff_oracle (\<^theory>, 2)\<close>
-ML \<open>iff_oracle (\<^theory>, 10)\<close>
-
-ML \<open>
-  \<^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>
-
-ML \<open>
-  (iff_oracle (\<^theory>, 5); error "Bad oracle")
-    handle Fail _ => writeln "Oracle failed, as expected"
-\<close>
-
-ML \<open>
-  (iff_oracle (\<^theory>, 1); error "Bad oracle")
-    handle Fail _ => writeln "Oracle failed, as expected"
-\<close>
-
-
-subsection \<open>Oracle as proof method\<close>
-
-method_setup iff =
-  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
-    SIMPLE_METHOD
-      (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
-        handle Fail _ => no_tac))\<close>
-
-
-lemma "A \<longleftrightarrow> A"
-  by (iff 2)
-
-lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
-  by (iff 10)
-
-lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
-  apply (iff 5)?
-  oops
-
-lemma A
-  apply (iff 1)?
-  oops
-
-end