src/Pure/theory.ML
changeset 8725 0e48ee5b52db
parent 6980 bb526ba7ba5f
child 8897 fb1436ca3b2e
equal deleted inserted replaced
8724:ef7efded8fdc 8725:0e48ee5b52db
    75   val add_defs: (bstring * string) list -> theory -> theory
    75   val add_defs: (bstring * string) list -> theory -> theory
    76   val add_defs_i: (bstring * term) list -> theory -> theory
    76   val add_defs_i: (bstring * term) list -> theory -> theory
    77   val add_path: string -> theory -> theory
    77   val add_path: string -> theory -> theory
    78   val parent_path: theory -> theory
    78   val parent_path: theory -> theory
    79   val root_path: theory -> theory
    79   val root_path: theory -> theory
    80   val add_space: string * string list -> theory -> theory
    80   val hide_space: string * xstring list -> theory -> theory
       
    81   val hide_space_i: string * string list -> theory -> theory
       
    82   val hide_classes: string list -> theory -> theory
       
    83   val hide_types: string list -> theory -> theory
       
    84   val hide_consts: string list -> theory -> theory
    81   val add_name: string -> theory -> theory
    85   val add_name: string -> theory -> theory
    82   val copy: theory -> theory
    86   val copy: theory -> theory
    83   val prep_ext: theory -> theory
    87   val prep_ext: theory -> theory
    84   val prep_ext_merge: theory list -> theory
    88   val prep_ext_merge: theory list -> theory
    85   val requires: theory -> string -> string -> unit
    89   val requires: theory -> string -> string -> unit
   145 
   149 
   146 
   150 
   147 
   151 
   148 (** extend theory **)
   152 (** extend theory **)
   149 
   153 
   150 (*name space kinds*)
   154 (*name spaces*)
   151 val axiomK = "axiom";
   155 val axiomK = "axiom";
   152 val oracleK = "oracle";
   156 val oracleK = "oracle";
   153 
   157 
   154 
   158 
   155 (* extend logical part of a theory *)
   159 (* extend logical part of a theory *)
   207 val add_trrules_i    = ext_sign Sign.add_trrules_i;
   211 val add_trrules_i    = ext_sign Sign.add_trrules_i;
   208 val add_path         = ext_sign Sign.add_path;
   212 val add_path         = ext_sign Sign.add_path;
   209 val parent_path      = add_path "..";
   213 val parent_path      = add_path "..";
   210 val root_path        = add_path "/";
   214 val root_path        = add_path "/";
   211 val add_space        = ext_sign Sign.add_space;
   215 val add_space        = ext_sign Sign.add_space;
       
   216 val hide_space       = ext_sign Sign.hide_space;
       
   217 val hide_space_i     = ext_sign Sign.hide_space_i;
       
   218 val hide_classes     = curry hide_space_i Sign.classK;
       
   219 val hide_types       = curry hide_space_i Sign.typeK;
       
   220 val hide_consts      = curry hide_space_i Sign.constK;
   212 val add_name         = ext_sign Sign.add_name;
   221 val add_name         = ext_sign Sign.add_name;
   213 val copy             = ext_sign (K Sign.copy) ();
   222 val copy             = ext_sign (K Sign.copy) ();
   214 val prep_ext         = ext_sign (K Sign.prep_ext) ();
   223 val prep_ext         = ext_sign (K Sign.prep_ext) ();
   215 
   224 
   216 
   225