# HG changeset patch
# User wenzelm
# Date 1138881139 -3600
# Node ID 9c8c60853966b6c66a50c18998a74d173574fde5
# Parent  2dbf73278b0ef761631446ab9e0e3494613bc712
added concluding statements: Shows/Obtains;

diff -r 2dbf73278b0e -r 9c8c60853966 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Feb 02 12:52:18 2006 +0100
+++ b/src/Pure/Isar/element.ML	Thu Feb 02 12:52:19 2006 +0100
@@ -33,6 +33,11 @@
   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 =
@@ -252,4 +257,15 @@
 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;