equal
deleted
inserted
replaced
10 (* The "expect" arguments to Nitpick in this theory and the other example |
10 (* The "expect" arguments to Nitpick in this theory and the other example |
11 theories are there so that the example can also serve as a regression test |
11 theories are there so that the example can also serve as a regression test |
12 suite. *) |
12 suite. *) |
13 |
13 |
14 theory Manual_Nits |
14 theory Manual_Nits |
15 imports Real "~~/src/HOL/Library/Quotient_Product" |
15 imports HOL.Real "HOL-Library.Quotient_Product" |
16 begin |
16 begin |
17 |
17 |
18 section \<open>2. First Steps\<close> |
18 section \<open>2. First Steps\<close> |
19 |
19 |
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |