# HG changeset patch
# User wenzelm
# Date 1416662016 -3600
# Node ID 67baff6f697cd4d619c66dbf53e44915d9196dc1
# Parent  c907cbe36713db29e38e9be7efc60654475bbca3
misc tuning and modernization;

diff -r c907cbe36713 -r 67baff6f697c src/HOL/ex/Iff_Oracle.thy
--- a/src/HOL/ex/Iff_Oracle.thy	Sat Nov 22 13:38:15 2014 +0100
+++ b/src/HOL/ex/Iff_Oracle.thy	Sat Nov 22 14:13:36 2014 +0100
@@ -3,21 +3,21 @@
     Author:     Makarius
 *)
 
-section {* Example of Declaring an Oracle *}
+section \<open>Example of Declaring an Oracle\<close>
 
 theory Iff_Oracle
 imports Main
 begin
 
-subsection {* Oracle declaration *}
+subsection \<open>Oracle declaration\<close>
 
-text {*
-  This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}.
+text \<open>
+  This oracle makes tautologies of the form @{prop "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"}.
   The length is specified by an integer, which is checked to be even
   and positive.
-*}
+\<close>
 
-oracle iff_oracle = {*
+oracle iff_oracle = \<open>
   let
     fun mk_iff 1 = Var (("P", 0), @{typ bool})
       | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1));
@@ -27,45 +27,48 @@
       then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
       else raise Fail ("iff_oracle: " ^ string_of_int n)
   end
-*}
+\<close>
 
 
-subsection {* Oracle as low-level rule *}
+subsection \<open>Oracle as low-level rule\<close>
+
+ML \<open>iff_oracle (@{theory}, 2)\<close>
+ML \<open>iff_oracle (@{theory}, 10)\<close>
 
-ML {* iff_oracle (@{theory}, 2) *}
-ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
-
-text {* These oracle calls had better fail. *}
+ML \<open>
+  Thm.peek_status (iff_oracle (@{theory}, 10));
+  @{assert} (#oracle it);
+\<close>
 
-ML {*
-  (iff_oracle (@{theory}, 5); error "Bad oracle")
-    handle Fail _ => warning "Oracle failed, as expected"
-*}
+text \<open>These oracle calls had better fail.\<close>
 
-ML {*
+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 _ => warning "Oracle failed, as expected"
-*}
+    handle Fail _ => writeln "Oracle failed, as expected"
+\<close>
 
 
-subsection {* Oracle as proof method *}
+subsection \<open>Oracle as proof method\<close>
 
-method_setup iff = {*
-  Scan.lift Parse.nat >> (fn n => fn ctxt =>
+method_setup iff =
+  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
     SIMPLE_METHOD
       (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
-        handle Fail _ => no_tac))
-*}
+        handle Fail _ => no_tac))\<close>
 
 
-lemma "A <-> A"
+lemma "A \<longleftrightarrow> A"
   by (iff 2)
 
-lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
+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 <-> A <-> A <-> A <-> A"
+lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
   apply (iff 5)?
   oops