# HG changeset patch # User blanchet # Date 1369119778 -7200 # Node ID f5280907284d1a53fd523897fc6cfca45d1b3b22 # Parent 895d12fc0dd7cd508ae7d1e2d130562472a49ccc added compatibility alias diff -r 895d12fc0dd7 -r f5280907284d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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"),