equal
deleted
inserted
replaced
10 theory Induct_Nits |
10 theory Induct_Nits |
11 imports Main |
11 imports Main |
12 begin |
12 begin |
13 |
13 |
14 nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI, |
14 nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI, |
15 max_threads = 1, timeout = 60 s] |
15 max_threads = 1, timeout = 60] |
16 |
16 |
17 inductive p1 :: "nat \<Rightarrow> bool" where |
17 inductive p1 :: "nat \<Rightarrow> bool" where |
18 "p1 0" | |
18 "p1 0" | |
19 "p1 n \<Longrightarrow> p1 (n + 2)" |
19 "p1 n \<Longrightarrow> p1 (n + 2)" |
20 |
20 |