equal
deleted
inserted
replaced
109 end |> Pretty.writeln_chunks |
109 end |> Pretty.writeln_chunks |
110 |
110 |
111 end |
111 end |
112 |
112 |
113 val _ = |
113 val _ = |
114 Outer_Syntax.command @{command_spec "find_unused_assms"} |
114 Outer_Syntax.command @{command_keyword find_unused_assms} |
115 "find theorems with (potentially) superfluous assumptions" |
115 "find theorems with (potentially) superfluous assumptions" |
116 (Scan.option Parse.name >> (fn name => |
116 (Scan.option Parse.name >> (fn name => |
117 Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
117 Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
118 |
118 |
119 end |
119 end |