# HG changeset patch
# User wenzelm
# Date 1152035396 -7200
# Node ID 3fd6d57b16dee1a29173acaec74f31a0345c83df
# Parent  e6d3f2b031e606d455b22aec5d4b08482e882135
Proof by guessing.

diff -r e6d3f2b031e6 -r 3fd6d57b16de src/HOL/ex/Guess.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Guess.thy	Tue Jul 04 19:49:56 2006 +0200
@@ -0,0 +1,31 @@
+(*
+    ID:         $Id$
+    Author:     Makarius
+*)
+
+header {* Proof by guessing *}
+
+theory Guess
+imports Main
+begin
+
+lemma True
+proof
+
+  have 1: "\<exists>x. x = x" by simp
+
+  from 1 guess ..
+  from 1 guess x ..
+  from 1 guess x :: 'a ..
+  from 1 guess x :: nat ..
+
+  have 2: "\<exists>x y. x = x & 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