--- a/src/HOL/ex/Guess.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Guess.thy Sat Nov 22 14:57:04 2014 +0100
@@ -8,9 +8,8 @@
imports Main
begin
-lemma True
-proof
-
+notepad
+begin
have 1: "\<exists>x. x = x" by simp
from 1 guess ..
@@ -18,13 +17,12 @@
from 1 guess x :: 'a ..
from 1 guess x :: nat ..
- have 2: "\<exists>x y. x = x & y = y" by simp
+ have 2: "\<exists>x y. x = x \<and> y = y" by simp
from 2 guess apply - apply (erule exE conjE)+ done
from 2 guess x apply - apply (erule exE conjE)+ done
from 2 guess x y apply - apply (erule exE conjE)+ done
from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
-
-qed
+end
end