419   Variable} from the @{ML_struct Variable} can be used to transfer

   419   Variable} from the structure @{ML_struct Variable} can be used to transfer

   425   variables (as can be seen by the leading question marks). Note that

   425   variables (as can be seen by the leading question marks in the result). 

   426   the variable @{text P} stays a free variable, since it not fixed in

   426   Note that the variable @{text P} stays a free variable, since it not fixed in

   436   structure @{ML_struct Skip_Proof} in order to turn an arbitray term,

   436   structure @{ML_struct Skip_Proof}. This function will turn an arbitray 

   437   in our case @{term "P x y z x y z"}, into a theorem.

   437   term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 

   438   whether it is actually provable).

   450   The result is that all variables are schematic. The great point about

   451   Since we fixed all variables in @{text ctxt1}, in result all of them 

   451   contexts is that exporting is not just concerned with variables, but

   452   are schematic. The great point is that exporting between contexts is 

   452   also assumptions. 

   453   not just concerned with variables, but also assumptions. For this we

   454   can use the function @{ML_ind export in Assumption} from the structure

   455   @{ML_struct Assumption}. Consider the following code.

   456 

   457   @{ML_response_fake [display, gray, linenos]

   458   "let

   459   val ctxt0 = @{context}

   460   val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0

   461   val eq' = Thm.symmetric eq

   462 in

   463   Assumption.export false ctxt1 ctxt0 eq'

   464 end"

   465   "x \<equiv> y \<Longrightarrow> y \<equiv> x"}

   466   

   467   The function @{ML_ind add_assumes in Assumption} from the structure

   468   @{ML_struct Assumption} adds the assumption \mbox{@{text "x \<equiv> y"}}

   469   to the context @{text ctxt1} (Line 3). This function expects a list

   470   of @{ML_type cterm}s and returns them as theorems, together with the

   471   new context in which they are ``assumed''. In Line 4 we use the

   472   function @{ML_ind symmetric in Thm} from the structure @{ML_struct

   473   Thm} in order to obtain the symmetric version of the assumed

   474   meta-equality. Now exporting the theorem @{text "eq'"} from @{text

   475   ctxt1} to @{text ctxt0} means @{term "y \<equiv> x"} will be prefixed with

   476   the assumed theorem. The boolean flag in @{ML_ind export in

   477   Assumption} indicates whether the assumptions should be marked with

   478   the goal marker (see Section~\ref{sec:basictactics}). In normal

   479   circumstances this is not necessary and so should be set to @{ML

   480   false}.  The result of the export is then the theorem \mbox{@{term

   481   "x \<equiv> y \<Longrightarrow> y \<equiv> x"}}.  As can be seen this is an easy way for obtaing

   482   simple theorems. We will explain this in more detail in

   483   Section~\ref{sec:structured}.

   484 

   485   The function @{ML_ind export in Proof_Context} from the structure 

   486   @{ML_struct Proof_Context} combines both export functions from 

   487   @{ML_struct Variable} and @{ML_struct Assumption}. This can be seen

   488   in the following example.

   489 

   490   @{ML_response_fake [display, gray]

   491   "let

   492   val ctxt0 = @{context}

   493   val ((fvs, [eq]), ctxt1) = ctxt0

   494     |> Variable.add_fixes [\"x\", \"y\"]

   495     ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]

   496   val eq' = Thm.symmetric eq

   497 in

   498   Proof_Context.export ctxt1 ctxt0 [eq']

   499 end"

   500   "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}