# HG changeset patch
# User webertj
# Date 1168453072 -3600
# Node ID 4b713f89f8c743f037ba7d3ae08f54f3da3ebee9
# Parent  792c18b8f214bf76e69ad737d01c4cd0ffeeed72
no unfolding necessary anymore (refute does that automatically now)

diff -r 792c18b8f214 -r 4b713f89f8c7 src/HOL/ex/Sudoku.thy
--- a/src/HOL/ex/Sudoku.thy	Wed Jan 10 09:28:24 2007 +0100
+++ b/src/HOL/ex/Sudoku.thy	Wed Jan 10 19:17:52 2007 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Sudoku.thy
     ID:         $Id$
     Author:     Tjark Weber
-    Copyright   2005
+    Copyright   2005-2007
 *)
 
 header {* A SAT-based Sudoku Solver *}
@@ -100,7 +100,6 @@
     x71 x72 x73 x74 x75 x76 x77 x78 x79
     x81 x82 x83 x84 x85 x86 x87 x88 x89
     x91 x92 x93 x94 x95 x96 x97 x98 x99"
-  apply (unfold sudoku_def valid_def)
   refute
 oops
 
@@ -118,7 +117,6 @@
     x71  6  x73 x74 x75 x76  2   8  x79
     x81 x82 x83  4   1   9  x87 x88  5 
     x91 x92 x93 x94  8  x96 x97  7   9 "
-  apply (unfold sudoku_def valid_def)
   refute
 oops
 
@@ -136,7 +134,6 @@
     x71 x72 x73 x74  1  x76  7   8  x79
      5  x82 x83 x84 x85  9  x87 x88 x89
     x91 x92 x93 x94 x95 x96 x97  4  x99"
-  apply (unfold sudoku_def valid_def)
   refute
 oops