changeset 59936 | b8ffc3dc9e24 |
parent 59582 | 0fbed69ff081 |
child 60638 | 16d80e5ef2dc |
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 17:06:48 2015 +0200 @@ -111,7 +111,7 @@ end val _ = - Outer_Syntax.command @{command_spec "find_unused_assms"} + Outer_Syntax.command @{command_keyword find_unused_assms} "find theorems with (potentially) superfluous assumptions" (Scan.option Parse.name >> (fn name => Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))