1.1 --- a/etc/isar-keywords-ZF.el	Thu Feb 28 16:54:56 2008 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Feb 28 17:33:35 2008 +0100
     1.3 @@ -193,6 +193,7 @@
     1.4      "undo"
     1.5      "undos_proof"
     1.6      "unfolding"
     1.7 +    "unused_thms"
     1.8      "use"
     1.9      "use_thy"
    1.10      "using"
    1.11 @@ -317,6 +318,7 @@
    1.12      "touch_child_thys"
    1.13      "touch_thy"
    1.14      "typ"
    1.15 +    "unused_thms"
    1.16      "use"
    1.17      "use_thy"
    1.18      "value"

     2.1 --- a/etc/isar-keywords.el	Thu Feb 28 16:54:56 2008 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Feb 28 17:33:35 2008 +0100
     2.3 @@ -235,6 +235,7 @@
     2.4      "undo"
     2.5      "undos_proof"
     2.6      "unfolding"
     2.7 +    "unused_thms"
     2.8      "use"
     2.9      "use_thy"
    2.10      "using"
    2.11 @@ -385,6 +386,7 @@
    2.12      "touch_child_thys"
    2.13      "touch_thy"
    2.14      "typ"
    2.15 +    "unused_thms"
    2.16      "use"
    2.17      "use_thy"
    2.18      "value"

     3.1 --- a/lib/jedit/isabelle.xml	Thu Feb 28 16:54:56 2008 +0100
     3.2 +++ b/lib/jedit/isabelle.xml	Thu Feb 28 17:33:35 2008 +0100
     3.3 @@ -323,6 +323,7 @@
     3.4        <INVALID>undo</INVALID>
     3.5        <INVALID>undos_proof</INVALID>
     3.6        <OPERATOR>unfolding</OPERATOR>
     3.7 +      <LABEL>unused_thms</LABEL>
     3.8        <LABEL>use</LABEL>
     3.9        <LABEL>use_thy</LABEL>
    3.10        <KEYWORD4>uses</KEYWORD4>

     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 16:54:56 2008 +0100
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 17:33:35 2008 +0100
     4.3 @@ -94,6 +94,8 @@
     4.4    val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     4.5    val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     4.6      -> Toplevel.transition -> Toplevel.transition
     4.7 +  val unused_thms: (string list * string list option) option ->
     4.8 +    Toplevel.transition -> Toplevel.transition
     4.9    val print_binds: Toplevel.transition -> Toplevel.transition
    4.10    val print_cases: Toplevel.transition -> Toplevel.transition
    4.11    val print_stmts: string list * (thmref * Attrib.src list) list
    4.12 @@ -531,6 +533,28 @@
    4.13    in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    4.14  
    4.15  
    4.16 +(* find unused theorems *)
    4.17 +
    4.18 +local
    4.19 +
    4.20 +fun pretty_name_thm (a, th) =
    4.21 +  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, Display.pretty_thm th];
    4.22 +
    4.23 +in
    4.24 +
    4.25 +fun unused_thms opt_range =
    4.26 +  Toplevel.keep (fn state => ThmDeps.unused_thms
    4.27 +    (case opt_range of
    4.28 +       NONE => (NONE, [Toplevel.theory_of state])
    4.29 +     | SOME (xs, NONE) =>
    4.30 +         (SOME (map ThyInfo.get_theory xs), [Toplevel.theory_of state])
    4.31 +     | SOME (xs, SOME ys) =>
    4.32 +        (SOME (map ThyInfo.get_theory xs), map ThyInfo.get_theory ys)) |>
    4.33 +           map pretty_name_thm |> Pretty.chunks |> Pretty.writeln);
    4.34 +
    4.35 +end;        
    4.36 +
    4.37 +
    4.38  (* print proof context contents *)
    4.39  
    4.40  val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>

     5.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 28 16:54:56 2008 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 28 17:33:35 2008 +0100
     5.3 @@ -924,6 +924,12 @@
     5.4        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
     5.5          (Code.print_codesetup o Toplevel.theory_of)));
     5.6  
     5.7 +val _ =
     5.8 +  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
     5.9 +    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
    5.10 +       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
    5.11 +         (Toplevel.no_timing oo IsarCmd.unused_thms));
    5.12 +
    5.13  
    5.14  (** system commands (for interactive mode only) **)
    5.15