added add_classrel;
authorwenzelm
Thu Jun 16 12:04:00 1994 +0200 (1994-06-16)
changeset 42195e1d4faa863
parent 420 1e0f1973536d
child 422 8f194014a9c8
added add_classrel;
src/Pure/sign.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jun 09 11:11:03 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jun 16 12:04:00 1994 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4      val certify_term: sg -> term -> term * typ * int
     1.5      val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.6      val add_classes: (class list * class * class list) list -> sg -> sg
     1.7 +    val add_classrel: (class * class) list -> sg -> sg
     1.8      val add_defsort: sort -> sg -> sg
     1.9      val add_types: (string * int * mixfix) list -> sg -> sg
    1.10      val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    1.11 @@ -78,7 +79,7 @@
    1.12  structure BasicSyntax: BASIC_SYNTAX = Syntax;
    1.13  structure Pretty = Syntax.Pretty;
    1.14  structure Type = Type;
    1.15 -open BasicSyntax Type;
    1.16 +open BasicSyntax (* FIXME *) Type;
    1.17  open Syntax.Mixfix;   (* FIXME *)
    1.18  
    1.19  
    1.20 @@ -266,9 +267,6 @@
    1.21    else
    1.22      extend_tsig tsig (map (fn (_, c, cs) => (c, cs)) classes, [], [], []);
    1.23  
    1.24 -fun ext_tsig_defsort tsig defsort =
    1.25 -  extend_tsig tsig ([], defsort, [], []);
    1.26 -
    1.27  fun ext_tsig_types tsig types =
    1.28    extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
    1.29  
    1.30 @@ -414,6 +412,12 @@
    1.31    end;
    1.32  
    1.33  
    1.34 +(* add to subclass relation *)
    1.35 +
    1.36 +fun ext_classrel (syn, tsig, ctab) pairs =
    1.37 +  (syn, ext_tsig_subclass tsig pairs, ctab);
    1.38 +
    1.39 +
    1.40  (* add syntactic translations *)
    1.41  
    1.42  fun ext_trfuns (syn, tsig, ctab) trfuns =
    1.43 @@ -445,6 +449,7 @@
    1.44  (* the external interfaces *)
    1.45  
    1.46  val add_classes   = extend_sign ext_classes "#";
    1.47 +val add_classrel  = extend_sign ext_classrel "#";
    1.48  val add_defsort   = extend_sign ext_defsort "#";
    1.49  val add_types     = extend_sign ext_types "#";
    1.50  val add_tyabbrs   = extend_sign ext_tyabbrs "#";
     2.1 --- a/src/Pure/thm.ML	Thu Jun 09 11:11:03 1994 +0200
     2.2 +++ b/src/Pure/thm.ML	Thu Jun 16 12:04:00 1994 +0200
     2.3 @@ -35,6 +35,7 @@
     2.4    (* FIXME *)
     2.5    local open Sign.Syntax Sign.Syntax.Mixfix in  (* FIXME remove ...Mixfix *)
     2.6      val add_classes: (class list * class * class list) list -> theory -> theory
     2.7 +    val add_classrel: (class * class) list -> theory -> theory
     2.8      val add_defsort: sort -> theory -> theory
     2.9      val add_types: (string * int * mixfix) list -> theory -> theory
    2.10      val add_tyabbrs: (string * string list * string * mixfix) list
    2.11 @@ -117,7 +118,7 @@
    2.12           bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
    2.13             -> cterm -> thm
    2.14    val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
    2.15 -  val rep_theory: theory -> {sign: Sign.sg, new_axioms: term Sign.Symtab.table, 
    2.16 +  val rep_theory: theory -> {sign: Sign.sg, new_axioms: term Sign.Symtab.table,
    2.17      parents: theory list}
    2.18    val subthy: theory * theory -> bool
    2.19    val eq_thy: theory * theory -> bool
    2.20 @@ -336,6 +337,7 @@
    2.21    ext_thy thy (extfun decls sign) [];
    2.22  
    2.23  val add_classes   = ext_sg Sign.add_classes;
    2.24 +val add_classrel  = ext_sg Sign.add_classrel;
    2.25  val add_defsort   = ext_sg Sign.add_defsort;
    2.26  val add_types     = ext_sg Sign.add_types;
    2.27  val add_tyabbrs   = ext_sg Sign.add_tyabbrs;