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/Nominal_Examples_Base.thy
author wenzelm
Sat, 04 Oct 2014 19:26:31 +0200
changeset 58538 299b82d12d53
parent 58329 a31404ec7414
child 58889 5b7a9633cfa8
permissions -rw-r--r--
proper treatment of @comment (amending 402a8e8107a7);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
diff changeset 
     1
 
(*  Author:  Christian Urban TU Muenchen *)
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
diff changeset 
     2
 












a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     3


header {* Various examples involving nominal datatypes. *}













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     4














a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     5


theory Nominal_Examples_Base













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     6


imports













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     7


  CK_Machine













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     8


  CR













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




     9


  CR_Takahashi













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    10


  Compile













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    11


  Contexts













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    12


  Crary













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    13


  Fsub













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    14


  Height













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    15


  Lambda_mu













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    16


  LocalWeakening













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    17


  Pattern













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    18


  SN













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    19


  SOS













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    20


  Standardization













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    21


  Support













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    22


  Type_Preservation













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    23


  W













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    24


  Weakening













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    25


begin













a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    26














a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'



blanchet


parents: 

diff
changeset




    27


end















isabelle