src/HOL/ex/Sudoku.thy
changeset 58310 91ea607a34d8
parent 58183 285fbec02fb0
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/ex/Sudoku.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/ex/Sudoku.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  no_notation Groups.one_class.one ("1")
     1.6  
     1.7 -datatype_new digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
     1.8 +datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
     1.9  
    1.10  definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where
    1.11