src/Pure/Isar/element.ML

   val instT_thm: theory -> typ Symtab.table -> thm -> thm
   val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i
   val inst_term: typ Symtab.table * term Symtab.table -> term -> term
   val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
   val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
+  datatype ('typ, 'term, 'att) stmt =
+    Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
+    Obtains of (string * ((string * 'typ option) list * 'term list)) list
+  type statement  (*= (string, string, Attrib.src) stmt*)
+  type statement_i  (*= (typ, term, attribute) stmt*)
 end;
 
 structure Element: ELEMENT =
 struct
 

     end;
 
 fun inst_ctxt thy envs =
   map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
 
+
+
+(** concluding statements **)
+
+datatype ('typ, 'term, 'att) stmt =
+  Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
+  Obtains of (string * ((string * 'typ option) list * 'term list)) list;
+
+type statement = (string, string, Attrib.src) stmt;
+type statement_i = (typ, term, attribute) stmt;
+
 end;