src/Pure/Tools/named_thms.ML
author wenzelm
Thu, 20 Mar 2008 16:04:34 +0100
changeset 26363 9d95309f8069
parent 24867 e5b55d7be9bb
child 26397 df68e8dfd0e3
permissions -rw-r--r--
export add/del_thm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24047
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Tools/named_thms.ML
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     4
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     5
Named collections of theorems in canonical order.
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     6
*)
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     7
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     8
signature NAMED_THMS =
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
     9
sig
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    10
  val get: Proof.context -> thm list
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    11
  val pretty: Proof.context -> Pretty.T
26363
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    12
  val add_thm: thm -> Context.generic -> Context.generic
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    13
  val del_thm: thm -> Context.generic -> Context.generic
24047
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    14
  val add: attribute
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    15
  val del: attribute
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    16
  val setup: theory -> theory
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    17
end;
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    18
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    19
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    20
struct
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    21
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    22
structure Data = GenericDataFun
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    23
(
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    24
  type T = thm list;
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    25
  val empty = [];
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    26
  val extend = I;
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    27
  fun merge _ = Thm.merge_thms;
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    28
);
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    29
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    30
val get = Data.get o Context.Proof;
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    31
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    32
fun pretty ctxt =
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    33
  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    34
26363
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    35
val add_thm = Data.map o Thm.add_thm;
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    36
val del_thm = Data.map o Thm.del_thm;
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    37
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    38
val add = Thm.declaration_attribute add_thm;
9d95309f8069 export add/del_thm;
wenzelm
parents: 24867
diff changeset
    39
val del = Thm.declaration_attribute del_thm;
24047
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    40
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    41
val setup =
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    42
  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    43
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24117
diff changeset
    44
val _ =
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24117
diff changeset
    45
  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
24117
94210ad252e3 added toplevel print command;
wenzelm
parents: 24047
diff changeset
    46
    OuterKeyword.diag
94210ad252e3 added toplevel print command;
wenzelm
parents: 24047
diff changeset
    47
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24117
diff changeset
    48
      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
24117
94210ad252e3 added toplevel print command;
wenzelm
parents: 24047
diff changeset
    49
24047
47b588ce11ec Named collections of theorems in canonical order.
wenzelm
parents:
diff changeset
    50
end;