src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 51189 a55ef201b19d
parent 51138 583a37b9512d
child 51190 2654b3965c8d
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 19 19:44:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -102,7 +102,8 @@
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
-   ("dont_preplay", ("preplay_timeout", ["0"]))]
+   ("dont_preplay", ("preplay_timeout", ["0"])),
+   ("dont_compress_isar", ("compress_isar", ["0"]))]
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),