src/Pure/CPure.thy
author wenzelm
Sat, 17 Sep 2005 18:11:28 +0200
changeset 17468 7c040a5fd171
parent 15804 3a55e6e26c8a
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
pretty_thm_aux: aconv hyps;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15804
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/CPure.thy
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     4
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     5
The CPure theory -- Pure with alternative application syntax.
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     6
*)
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     7
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     8
theory CPure
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     9
imports Pure
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    10
begin
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    11
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    12
setup
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    13
"[Theory.del_modesyntax Syntax.default_mode Syntax.pure_appl_syntax,
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    14
  Theory.add_syntax Syntax.pure_applC_syntax]"
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    15
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    16
end