equal
deleted
inserted
replaced
15 imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF" |
15 imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF" |
16 begin |
16 begin |
17 |
17 |
18 chapter {* 2. First Steps *} |
18 chapter {* 2. First Steps *} |
19 |
19 |
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
20 nitpick_params [sat_solver = Riss3g, max_threads = 1, timeout = 240] |
21 |
21 |
22 subsection {* 2.1. Propositional Logic *} |
22 subsection {* 2.1. Propositional Logic *} |
23 |
23 |
24 lemma "P \<longleftrightarrow> Q" |
24 lemma "P \<longleftrightarrow> Q" |
25 nitpick [expect = genuine] |
25 nitpick [expect = genuine] |