# HG changeset patch
# User wenzelm
# Date 1138727975 -3600
# Node ID 7aa8cd3812d3b2e19dc0fb6a642309b03273010c
# Parent  08b06ec0ef74597122b178cb0284916dbb5666ec
improved comments;

diff -r 08b06ec0ef74 -r 7aa8cd3812d3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jan 31 18:19:34 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 31 18:19:35 2006 +0100
@@ -1220,9 +1220,23 @@
 
 (* basic assumptions *)
 
+(*
+    [A]
+     : 
+     B
+  --------
+  #A ==> B
+*)
 fun assume_export true = Seq.single oo Drule.implies_intr_protected
   | assume_export false = Seq.single oo Drule.implies_intr_list;
 
+(*
+    [A]
+     : 
+     B
+  -------
+  A ==> B
+*)
 fun presume_export _ = assume_export false;