src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 45707 6bf7eec9b153
parent 45706 418846ea4f99
child 45781 fc2c368b5f54
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:14 2011 +0100
@@ -34,6 +34,7 @@
      isar_proof: bool,
      isar_shrink_factor: int,
      slice: bool,
+     minimize: bool option,
      timeout: Time.time,
      preplay_timeout: Time.time,
      expect: string}
@@ -297,6 +298,7 @@
    isar_proof: bool,
    isar_shrink_factor: int,
    slice: bool,
+   minimize: bool option,
    timeout: Time.time,
    preplay_timeout: Time.time,
    expect: string}