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
Tue, 11 Nov 2014 18:16:25 +0100
changeset 58978 e42da880c61e
parent 58889 5b7a9633cfa8
permissions -rw-r--r--
more position information, e.g. relevant for errors in generated ML source;
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
 







58889






5b7a9633cfa8
modernized header uniformly as section;



wenzelm


parents: 
58329

diff
changeset




     3


section {* Various examples involving nominal datatypes. *}








58329






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