author | haftmann |
Wed, 13 Jul 2005 11:30:37 +0200 | |
changeset 16790 | be2780f435e1 |
parent 15804 | 3a55e6e26c8a |
child 18019 | d1ff9ebb8bcb |
permissions | -rw-r--r-- |
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 |