Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
changeset 54838 16511f84913c
parent 54816 10d48c2a3e32
child 55193 78eb7fab3284 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Dec 20 20:36:38 2013 +0100
@@ -20,8 +20,8 @@
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
       (facts * proof_method list list)
   and proof_method =
-    Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
-    Force_Method | Arith_Method | Blast_Method | Meson_Method
+    Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+    Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
 
   val no_label : label
   val no_facts : facts
@@ -69,8 +69,8 @@
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     (facts * proof_method list list)
 and proof_method =
-  Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
-  Force_Method | Arith_Method | Blast_Method | Meson_Method
+  Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+  Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
 
 val no_label = ("", ~1)
 val no_facts = ([],[])
isabelle