Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/CPure.thy
author wenzelm
Tue, 07 Feb 2006 19:56:49 +0100
changeset 18967 ea42ab6c08d1
parent 18835 8e080d0252c5
child 19048 2b875dd5eb4c
permissions -rw-r--r--
export consts_of; removed const_expansion; pretty_term', infer_types(_simult): separate Consts.T argument; added generic certify; simplified certify_term/prop;
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















isabelle