src/Pure/CPure.thy
author wenzelm
Wed, 02 Aug 2006 22:27:02 +0200
changeset 20308 ddb7e7129481
parent 19048 2b875dd5eb4c
child 26435 bdce320cd426
permissions -rw-r--r--
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 CPure
imports Pure
begin

setup  -- {* Some syntax modifications, see ROOT.ML *}

end