src/Pure/CPure.thy
author wenzelm
Fri, 06 Jan 2006 18:18:13 +0100
changeset 18595 a52907967bae
parent 18019 d1ff9ebb8bcb
child 18709 f174ebc26073
permissions -rw-r--r--
simplified EqSubst setup;
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
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     4
The CPure theory -- Pure with alternative application syntax.
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     5
*)
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
theory CPure
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     8
imports Pure
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
     9
begin
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    10
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    11
setup
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    12
"[Theory.del_modesyntax Syntax.default_mode Syntax.pure_appl_syntax,
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    13
  Theory.add_syntax Syntax.pure_applC_syntax]"
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    14
3a55e6e26c8a The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff changeset
    15
end