src/Pure/Isar/element.ML
changeset 18894 9c8c60853966
parent 18669 cd6d6baf0411
child 18906 2487aea6ff12
     1.1 --- a/src/Pure/Isar/element.ML	Thu Feb 02 12:52:18 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Feb 02 12:52:19 2006 +0100
     1.3 @@ -33,6 +33,11 @@
     1.4    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
     1.5    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
     1.6    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
     1.7 +  datatype ('typ, 'term, 'att) stmt =
     1.8 +    Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
     1.9 +    Obtains of (string * ((string * 'typ option) list * 'term list)) list
    1.10 +  type statement  (*= (string, string, Attrib.src) stmt*)
    1.11 +  type statement_i  (*= (typ, term, attribute) stmt*)
    1.12  end;
    1.13  
    1.14  structure Element: ELEMENT =
    1.15 @@ -252,4 +257,15 @@
    1.16  fun inst_ctxt thy envs =
    1.17    map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
    1.18  
    1.19 +
    1.20 +
    1.21 +(** concluding statements **)
    1.22 +
    1.23 +datatype ('typ, 'term, 'att) stmt =
    1.24 +  Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
    1.25 +  Obtains of (string * ((string * 'typ option) list * 'term list)) list;
    1.26 +
    1.27 +type statement = (string, string, Attrib.src) stmt;
    1.28 +type statement_i = (typ, term, attribute) stmt;
    1.29 +
    1.30  end;