removed attribute.ML;
authorwenzelm
Tue Jan 12 12:28:29 1999 +0100 (1999-01-12)
changeset 6083ede76e7af057
parent 6082 590f9e3bf4d8
child 6084 842b059e023f
removed attribute.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/attribute.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Jan 12 12:17:53 1999 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Tue Jan 12 12:28:29 1999 +0100
     1.3 @@ -38,11 +38,11 @@
     1.4    Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
     1.5    Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML \
     1.6    Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
     1.7 -  Thy/thy_syn.ML Thy/use.ML attribute.ML axclass.ML basis.ML deriv.ML \
     1.8 -  display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \
     1.9 -  locale.ML logic.ML net.ML object_logic.ML pattern.ML pure.ML \
    1.10 -  pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML \
    1.11 -  theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    1.12 +  Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
    1.13 +  drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
    1.14 +  logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \
    1.15 +  search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
    1.16 +  theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    1.17  	@./mk
    1.18  
    1.19  
     2.1 --- a/src/Pure/ROOT.ML	Tue Jan 12 12:17:53 1999 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Tue Jan 12 12:28:29 1999 +0100
     2.3 @@ -39,7 +39,6 @@
     2.4  use "object_logic.ML";
     2.5  use "thm.ML";
     2.6  use "display.ML";
     2.7 -use "attribute.ML";
     2.8  use "pure_thy.ML";
     2.9  use "deriv.ML";
    2.10  use "drule.ML";
     3.1 --- a/src/Pure/attribute.ML	Tue Jan 12 12:17:53 1999 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,107 +0,0 @@
     3.4 -(*  Title:      Pure/attribute.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -Theorem tags and attributes.
     3.9 -*)
    3.10 -
    3.11 -signature BASIC_ATTRIBUTE =
    3.12 -sig
    3.13 -  type tag
    3.14 -  type tthm
    3.15 -  type 'a attribute
    3.16 -  val show_tags: bool ref
    3.17 -end;
    3.18 -
    3.19 -signature ATTRIBUTE =
    3.20 -sig
    3.21 -  include BASIC_ATTRIBUTE
    3.22 -  val thm_of: tthm -> thm
    3.23 -  val tthm_of: thm -> tthm
    3.24 -  val thms_of: tthm list -> thm list
    3.25 -  val tthms_of: thm list -> tthm list
    3.26 -  val rule: ('a -> thm -> thm) -> 'a attribute
    3.27 -  val none: 'a -> 'a * 'b attribute list
    3.28 -  val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
    3.29 -  val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
    3.30 -  val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
    3.31 -  val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
    3.32 -  val pretty_tthm: tthm -> Pretty.T
    3.33 -  val pretty_tthms: tthm list -> Pretty.T
    3.34 -  val print_tthm: tthm -> unit
    3.35 -  val print_tthms: tthm list -> unit
    3.36 -  val tag: tag -> 'a attribute
    3.37 -  val untag: tag -> 'a attribute
    3.38 -  val lemma: tag
    3.39 -  val assumption: tag
    3.40 -  val internal: tag
    3.41 -  val tag_lemma: 'a attribute
    3.42 -  val tag_assumption: 'a attribute
    3.43 -  val tag_internal: 'a attribute
    3.44 -end;
    3.45 -
    3.46 -structure Attribute: ATTRIBUTE =
    3.47 -struct
    3.48 -
    3.49 -
    3.50 -(** tags and attributes **)
    3.51 -
    3.52 -type tag = string * string list;
    3.53 -type tthm = thm * tag list;
    3.54 -type 'a attribute = 'a * tthm -> 'a * tthm;
    3.55 -
    3.56 -fun thm_of (thm, _) = thm;
    3.57 -fun tthm_of thm = (thm, []);
    3.58 -
    3.59 -fun thms_of ths = map thm_of ths;
    3.60 -fun tthms_of ths = map tthm_of ths;
    3.61 -
    3.62 -fun rule f (x, (thm, _)) = (x, (f x thm, []));
    3.63 -
    3.64 -fun none x = (x, []);
    3.65 -fun no_attrs (x, y) = ((x, (y, [])), []);
    3.66 -fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
    3.67 -
    3.68 -
    3.69 -(* apply attributes *)
    3.70 -
    3.71 -fun apply (x_th, atts) = Library.apply atts x_th;
    3.72 -fun applys (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
    3.73 -
    3.74 -
    3.75 -(* display tagged theorems *)
    3.76 -
    3.77 -val show_tags = ref false;
    3.78 -
    3.79 -fun pretty_tag (name, args) = Pretty.strs (name :: args);
    3.80 -val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    3.81 -
    3.82 -fun pretty_tthm (thm, tags) =
    3.83 -  if null tags orelse not (! show_tags) then Pretty.quote (Display.pretty_thm thm)
    3.84 -  else Pretty.block [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
    3.85 -
    3.86 -fun pretty_tthms [th] = pretty_tthm th
    3.87 -  | pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));
    3.88 -
    3.89 -val print_tthm = Pretty.writeln o pretty_tthm;
    3.90 -val print_tthms = Pretty.writeln o pretty_tthms;
    3.91 -
    3.92 -
    3.93 -(* basic attributes *)
    3.94 -
    3.95 -fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
    3.96 -fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
    3.97 -
    3.98 -val lemma = ("lemma", []);
    3.99 -val assumption = ("assumption", []);
   3.100 -val internal = ("internal", []);
   3.101 -fun tag_lemma x = tag lemma x;
   3.102 -fun tag_assumption x = tag assumption x;
   3.103 -fun tag_internal x = tag internal x;
   3.104 -
   3.105 -
   3.106 -end;
   3.107 -
   3.108 -
   3.109 -structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
   3.110 -open BasicAttribute;