# HG changeset patch
# User webertj
# Date 1079084879 -3600
# Node ID 8cc21ed7ef41a9127a55cad9945ee439c957dc88
# Parent  72ad5f2a38039e4608ff35ba38af60e7d2d9298b
\<dots> replaced by ...

diff -r 72ad5f2a3803 -r 8cc21ed7ef41 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Mar 11 13:34:13 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Mar 12 10:47:59 2004 +0100
@@ -22,8 +22,8 @@
   refute 2  -- {* refutes @{term "Q"} *}
   refute    -- {* equivalent to 'refute 1' *}
     -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
-  refute [maxsize=5]           -- {* we can override parameters \<dots> *}
-  refute [satsolver="dpll"] 2  -- {* \<dots> and specify a subgoal at the same time *}
+  refute [maxsize=5]           -- {* we can override parameters ... *}
+  refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
 oops
 
 refute_params
@@ -175,14 +175,14 @@
   (* refute -- works well with ZChaff, but the internal solver is too slow *)
 oops
 
-text {* The "Drinker's theorem" \<dots> *}
+text {* The "Drinker's theorem" ... *}
 
 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
   refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
   apply (auto simp add: ext)
 done
 
-text {* \<dots> and an incorrect version of it *}
+text {* ... and an incorrect version of it *}
 
 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   refute
@@ -285,13 +285,13 @@
   apply simp
 done
 
-text {* Axiom of Choice: first an incorrect version \<dots> *}
+text {* Axiom of Choice: first an incorrect version ... *}
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   refute
 oops
 
-text {* \<dots> and now two correct ones *}
+text {* ... and now two correct ones *}
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   refute [maxsize=5]