| author | huffman |
| Thu, 26 May 2005 02:23:27 +0200 | |
| changeset 16081 | 81a4b4a245b0 |
| 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 |