equal
deleted
inserted
replaced
8 header {* Examples Featuring Nitpick Applied to Datatypes *} |
8 header {* Examples Featuring Nitpick Applied to Datatypes *} |
9 |
9 |
10 theory Datatype_Nits |
10 theory Datatype_Nits |
11 imports Main |
11 imports Main |
12 begin |
12 begin |
|
13 |
|
14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] |
13 |
15 |
14 primrec rot where |
16 primrec rot where |
15 "rot Nibble0 = Nibble1" | |
17 "rot Nibble0 = Nibble1" | |
16 "rot Nibble1 = Nibble2" | |
18 "rot Nibble1 = Nibble2" | |
17 "rot Nibble2 = Nibble3" | |
19 "rot Nibble2 = Nibble3" | |