# HG changeset patch
# User wenzelm
# Date 1003872569 -7200
# Node ID dfdf0798d7b85cd917f9fa137be63b830c9d2abd
# Parent  9a0a736d820bb19a538d9dc3df2a1295804e358d
added export_assume, export_presume, export_def (from proof.ML);

diff -r 9a0a736d820b -r dfdf0798d7b8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 23 23:28:59 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 23 23:29:29 2001 +0200
@@ -77,6 +77,9 @@
   val have_thmss:
     ((string * context attribute list) * (thm list * context attribute list) list) list ->
       context -> context * (string * thm list) list
+  val export_assume: exporter
+  val export_presume: exporter
+  val export_def: exporter
   val assume: exporter
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> context -> context * ((string * thm list) list * thm list)
@@ -832,6 +835,28 @@
 
 (** assumptions **)
 
+(* basic exporters *)
+
+fun export_assume true = Seq.single oo Drule.implies_intr_goals
+  | export_assume false = Seq.single oo Drule.implies_intr_list;
+
+fun export_presume _ = export_assume false;
+
+
+fun dest_lhs cprop =
+  let val x = #1 (Logic.dest_equals (Thm.term_of cprop))
+  in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
+  handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
+      quote (Display.string_of_cterm cprop), []);
+
+fun export_def _ cprops thm =
+  thm
+  |> Drule.implies_intr_list cprops
+  |> Drule.forall_intr_list (map dest_lhs cprops)
+  |> Drule.forall_elim_vars 0
+  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
+
+
 (* assume *)
 
 local