# HG changeset patch # User webertj # Date 1079084879 -3600 # Node ID 8cc21ed7ef41a9127a55cad9945ee439c957dc88 # Parent 72ad5f2a38039e4608ff35ba38af60e7d2d9298b \ 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 \ *} - refute [satsolver="dpll"] 2 -- {* \ 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" \ *} +text {* The "Drinker's theorem" ... *} lemma "\x. f x = g x \ f = g" refute [maxsize=4] (* [maxsize=6] works well with ZChaff *) apply (auto simp add: ext) done -text {* \ and an incorrect version of it *} +text {* ... and an incorrect version of it *} lemma "(\x. f x = g x) \ f = g" refute @@ -285,13 +285,13 @@ apply simp done -text {* Axiom of Choice: first an incorrect version \ *} +text {* Axiom of Choice: first an incorrect version ... *} lemma "(\x. \y. P x y) \ (EX!f. \x. P x (f x))" refute oops -text {* \ and now two correct ones *} +text {* ... and now two correct ones *} lemma "(\x. \y. P x y) \ (\f. \x. P x (f x))" refute [maxsize=5]