Solved one of the strong-induction goals.

avoiding for atom.

Started proving strong induction.

stating the strong induction; further.

Working on stating induct.

some tuning; possible fix for strange paper generation

more on the paper

merge

Showed support of Core Haskell

Support proof modification for Core Haskell.

Experiments with Core Haskell support.

Export all the cheats needed for Core Haskell.

Compute Fv for non-recursive bn functions calling other bn functions

Core Haskell experiments.

tuned paper

more of the paper

merged

more tuning in the paper

merge

Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.

merged

more tuning

tuned paper

more on the paper

merge

Modification to Core Haskell to make it accepted with an empty binding function.

merged

tuned paper

Initial list unfoldings in Core Haskell.

compiles

More modification needed for compilation

Moved let properties from Term5 to ExLetRec.

Move Let properties to ExLet

Added missing file

More reorganization.

Move Leroy out of Test, rename accordingly.

Term1 is identical to Example 3

Move example3 out.

Move Ex1 and Ex2 out of Test

Move examples which create more permutations out

Move LamEx out of Test.

Move lambda examples to manual

Move manual examples to a subdirectory.

Removed compat tests.

merge

Move Non-respectful examples to NotRsp

merged

more on the paper

Move the comment to appropriate place.

Remove compose_eqvt

sym proof with compose.

Marked the place where a compose lemma applies.

merge

equivp_cheat can be removed for all one-permutation examples.

merged

more on the paper

merged

tuned paper

Got rid of alpha_bn_rsp_cheat.

alpha_bn_rsp_pre automatized.

merge

fv_rsp proved automatically.

more on the paper

merged

tuned paper

some tuning

Strong induction for Type Schemes.

Fixed missing colon.

tuned paper

merged

proved at_set_avoiding2 which is needed for strong induction principles

moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp

Size experiments.

Use 'alpha_bn_refl' to get rid of one of the sorrys.

Build alpha-->alphabn implications

Prove reflp for all relations.

started cleaning up and introduced 3 versions of ~~gen

moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas

more work on the paper

Described automatically created funs.

merge

Automatically derive support for datatypes with at-most one binding per constructor.

picture

merged

polished

Update Test to use fset.

merge

Use fs typeclass in showing finite support + some cheat cleaning.

merged

more one the paper

Keep only one copy of infinite_Un.

Added a missing 'import'.

Showed the instance: fset::(at) fs

merge

Remove atom_decl from the parser.

TySch strong induction looks ok.

Working on TySch strong induction.

Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...

merged

more tuning on the paper

The nominal infrastructure for fset. 'fs' missing, but not needed so far.

A few more theorems in FSet.

merge 2

merge 1

support of fset_to_set, support of fmap_atom.

merged

more tuning on the paper

added item about size functions

merge

Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.

tuned

another little bit for the introduction

Leroy96 supp=fv and fixes to make it compile

merged

more of the introduction

merge

Added a cleaned version of FSet.

corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant

Continued description of alpha.

Rename "_property" to ".property"