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/HOL/Nominal/Examples/ROOT.ML
author urbanc
Fri, 02 Feb 2007 17:16:16 +0100
changeset 22231 f76f187c91f9
parent 22073 c170dcbe6c9d
child 22448 f982e73e36de
permissions -rw-r--r--
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19495
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset 
     1
 
(*  Title:      HOL/Nominal/Examples/ROOT.ML
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset 
     2
 
    ID:         $Id$
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset 
     3
 
    Author:     Christian Urban, TU Muenchen
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset 
     4
 












3d04b87ad8ba
New ROOT file for nominal datatype examples.



berghofe


parents: 

diff
changeset




     5


Various examples involving nominal datatypes.













3d04b87ad8ba
New ROOT file for nominal datatype examples.



berghofe


parents: 

diff
changeset




     6


*)













3d04b87ad8ba
New ROOT file for nominal datatype examples.



berghofe


parents: 

diff
changeset




     7














3d04b87ad8ba
New ROOT file for nominal datatype examples.



berghofe


parents: 

diff
changeset




     8


use_thy "CR";








19499






1a082c1257d7
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.



berghofe


parents: 
19495

diff
changeset




     9


use_thy "Class";








21086






fe9f43a1e5bd
Added Compile and Height examples.



berghofe


parents: 
19499

diff
changeset




    10


use_thy "Compile";













fe9f43a1e5bd
Added Compile and Height examples.



berghofe


parents: 
19499

diff
changeset




    11


use_thy "Fsub";













fe9f43a1e5bd
Added Compile and Height examples.



berghofe


parents: 
19499

diff
changeset




    12


use_thy "Height";








19499






1a082c1257d7
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.



berghofe


parents: 
19495

diff
changeset




    13


use_thy "Lambda_mu";













1a082c1257d7
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.



berghofe


parents: 
19495

diff
changeset




    14


use_thy "SN";








19495






3d04b87ad8ba
New ROOT file for nominal datatype examples.



berghofe


parents: 

diff
changeset




    15


use_thy "Weakening";








22073






c170dcbe6c9d
formalisation of Crary's chapter on logical relations



urbanc


parents: 
21136

diff
changeset




    16


use_thy "Crary";














isabelle