src/Pure/CPure.thy
author obua
Mon, 13 Jun 2005 21:28:57 +0200
changeset 16384 90c51c932154
parent 15804 3a55e6e26c8a
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
internalize axiom names in Defs.define; compress types via Term.compress_type

(*  Title:      Pure/CPure.thy
    ID:         $Id$
    Author:     Makarius

The CPure theory -- Pure with alternative application syntax.
*)

theory CPure
imports Pure
begin

setup
"[Theory.del_modesyntax Syntax.default_mode Syntax.pure_appl_syntax,
  Theory.add_syntax Syntax.pure_applC_syntax]"

end