
diff -r 73c1ad6eda9d -r 351c63bb2704 doc-src/IsarImplementation/Thy/unused.thy
--- a/doc-src/IsarImplementation/Thy/unused.thy	Fri Sep 01 20:40:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/unused.thy	Fri Sep 01 20:44:16 2006 +0200
@@ -1,5 +1,15 @@
 
 text {*
+
+  @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
+
+
+
+  \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
+  Variable.export}, i.e.\ it provides a view on facts with all
+  variables being fixed in the current context.
+
+
   In practice, super-contexts emerge either by merging existing ones,
   or by adding explicit declarations.  For example, new theories are
   usually derived by importing existing theories from the library




