author | blanchet |
Fri, 15 Feb 2013 09:17:26 +0100 | |
changeset 51138 | 583a37b9512d |
parent 51137 | 077456580eca |
child 51140 | 59e311235de4 |
child 51145 | 280ece22765b |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Feb 15 09:17:20 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Feb 15 09:17:26 2013 +0100 @@ -101,8 +101,7 @@ ("preplay_timeout", "3")] val alias_params = - [("prover", ("provers", [])), (* legacy *) - ("max_relevant", ("max_facts", [])), (* legacy *) + [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"]))] val negated_alias_params = [("no_debug", "debug"),