--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 20 20:54:11 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 21 09:02:58 2013 +0200
@@ -108,7 +108,8 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
("dont_preplay", ("preplay_timeout", ["0"])),
- ("dont_compress_isar", ("isar_compress", ["0"]))]
+ ("dont_compress_isar", ("isar_compress", ["0"])),
+ ("isar_proof", ("isar_proofs", [])) (* legacy *)]
val negated_alias_params =
[("no_debug", "debug"),
("quiet", "verbose"),