added tactical result;
simplified obtain_export: no Seq.seq, no lifting of result prems;
tuned;
(* Title: Pure/CPure.thy ID: $Id$The CPure theory -- Pure with alternative application syntax.*)theory CPureimports Purebeginsetup -- {* Some syntax modifications, see ROOT.ML *}end