src/Pure/CPure.thy
author wenzelm
Thu, 28 Jul 2005 15:20:03 +0200
changeset 16946 7f9a7fe413f3
parent 15804 3a55e6e26c8a
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;
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