src/Pure/CPure.thy
author wenzelm
Sun, 29 Jan 2006 19:23:42 +0100
changeset 18835 8e080d0252c5
parent 18709 f174ebc26073
child 19048 2b875dd5eb4c
permissions -rw-r--r--
implicit 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
18835
8e080d0252c5 implicit setup;
wenzelm
parents: 18709
diff changeset
    11
subsection {* Specific modifications, see ROOT.ML *}
8e080d0252c5 implicit setup;
wenzelm
parents: 18709
diff changeset
    12
8e080d0252c5 implicit setup;
wenzelm
parents: 18709
diff changeset
    13
setup
15804
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