# HG changeset patch
# User blanchet
# Date 1409824419 -7200
# Node ID 285fbec02fb01ef123ae8824cf342381f179567b
# Parent  82478e6c60cb4b4e3c02177be8b2590915fdb469
tuned Nitpick and Refute examples, which are too slow on some testing machines

diff -r 82478e6c60cb -r 285fbec02fb0 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Sep 04 11:20:59 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Sep 04 11:53:39 2014 +0200
@@ -1207,27 +1207,6 @@
 
 (*****************************************************************************)
 
-subsubsection {* Records *}
-
-(*TODO: make use of pair types, rather than typedef, for record types*)
-
-record ('a, 'b) point =
-  xpos :: 'a
-  ypos :: 'b
-
-lemma "(x::('a, 'b) point) = y"
-refute [expect = genuine]
-oops
-
-record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
-  ext :: 'c
-
-lemma "(x::('a, 'b, 'c) extpoint) = y"
-refute [expect = genuine]
-oops
-
-(*****************************************************************************)
-
 subsubsection {* Examples involving special functions *}
 
 lemma "card x = 0"
diff -r 82478e6c60cb -r 285fbec02fb0 src/HOL/ex/Sudoku.thy
--- a/src/HOL/ex/Sudoku.thy	Thu Sep 04 11:20:59 2014 +0200
+++ b/src/HOL/ex/Sudoku.thy	Thu Sep 04 11:53:39 2014 +0200
@@ -19,7 +19,7 @@
 
 no_notation Groups.one_class.one ("1")
 
-datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
+datatype_new digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
 
 definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where