improved comments;

--- 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;