changeset 57263 | 2b6a96cc64c9 |
parent 57262 | b2c629647a14 |
child 57265 | cab38f7a3adb |
--- a/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:59 2014 +0200 @@ -33,4 +33,8 @@ ML_file "Tools/Sledgehammer/sledgehammer.ML" ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" +lemma "1 + 1 = (2::nat)" +sledgehammer [vampire, max_facts = 3] +oops + end