equal
deleted
inserted
replaced
7 theory SMT_Examples |
7 theory SMT_Examples |
8 imports Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 declare [[smt_solver=z3, smt_oracle=false]] |
11 declare [[smt_solver=z3, smt_oracle=false]] |
12 declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Examples.certs"]] |
12 declare [[smt_certificates="SMT_Examples.certs"]] |
13 declare [[smt_fixed=true]] |
13 declare [[smt_fixed=true]] |
14 |
14 |
15 |
15 |
16 |
16 |
17 section {* Propositional and first-order logic *} |
17 section {* Propositional and first-order logic *} |