Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.

Update cheats in TODO.

Removed another cheat and cleaned the code a bit.

Fix Manual/LamEx for experiments.

Proper bn_rsp, for bn functions calling each other.

Gathering things to prove by induction together; removed cheat_bn_eqvt.

Update TODO

Showed ACons_subst.

Only ACons_subst left to show.

Solved all boring subgoals, and looking at properly defning permute_bv

One more copy-and-paste in core-haskell.

Properly defined permute_bn. No more sorry's in Let strong induction.

Showed Let substitution.

Only let substitution is left.

further in the proof

trying to prove the string induction for let.

added experiemental permute_bn

first attempt of strong induction for lets with assignments

more on the paper

more on the paper

Further in the strong induction proof.

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.