author | wenzelm |
Thu, 27 Mar 2008 17:35:56 +0100 | |
changeset 26439 | e38f7e1c07ce |
parent 26435 | bdce320cd426 |
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 |
|
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 |
|
26435 | 11 |
no_syntax |
12 |
"_appl" :: "('b => 'a) => args => logic" ("(1_/(1'(_')))" [1000, 0] 1000) |
|
13 |
"_appl" :: "('b => 'a) => args => aprop" ("(1_/(1'(_')))" [1000, 0] 1000) |
|
14 |
||
15 |
syntax |
|
16 |
"" :: "'a => cargs" ("_") |
|
17 |
"_cargs" :: "'a => cargs => cargs" ("_/ _" [1000, 1000] 1000) |
|
18 |
"_applC" :: "('b => 'a) => cargs => logic" ("(1_/ _)" [1000, 1000] 999) |
|
19 |
"_applC" :: "('b => 'a) => cargs => aprop" ("(1_/ _)" [1000, 1000] 999) |
|
15804
3a55e6e26c8a
The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff
changeset
|
20 |
|
3a55e6e26c8a
The CPure theory -- Pure with alternative application syntax.
wenzelm
parents:
diff
changeset
|
21 |
end |