equal
deleted
inserted
replaced
32 ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
32 ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
33 ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
33 ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
34 ML_file "Tools/Sledgehammer/sledgehammer.ML" |
34 ML_file "Tools/Sledgehammer/sledgehammer.ML" |
35 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" |
35 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" |
36 |
36 |
|
37 definition plus1 where "plus1 x = x + (1::int)" |
|
38 |
|
39 ML {* print_depth 1000 *} |
|
40 |
|
41 lemma "map plus1 [0] = [1]" |
|
42 sledgehammer [z3_new, isar_proofs = true, mepo, debug, dont_preplay, dont_minimize, dont_try0_isar] |
|
43 (add: plus1_def) |
|
44 oops |
|
45 |
37 end |
46 end |