removed "raw" distinction

More on Section 5

Beginning of section 5.

merged

Avoid mentioning other nominal datatypes as it makes things too complicated.

merged

close the missing parenthesis on both sides.

merged

changes to section 2

Clean alpha

clean fv_bn

alpha_bn

Change @{text} to @{term}

alpha

more

fv and fv_bn

more of the paper

merged

Updated strong induction to modified definitions.

Initial renaming

small changes in the core-haskell spec

Update according to paper

merge

merge

Changed to Lists.

clarified core-haskell example

spell check

merge

Abs_gen and Abs_let simplifications.

more on the paper

fixed a problem due to a change in type-def (needs new Isabelle)

merged

more on the paper

got rid of the aux-function on the raw level, by defining it with function on the quotient level

Lets finally abstract lists.

Core Haskell can now use proper strings.

Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.

Remove list_eq notation.

Get lifted types information from the quotient package.

Equivariance when bn functions are lists.

Accepts lists in FV.

Parsing of list-bn functions into components.

Automatically compute support if only one type of Abs is present in the type.

Manually proved TySch support; All properties of TySch now true.

Generalize Abs_eq_iff.

Minor fix.

New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.

Initial proof modifications for alpha_res

merge

Fv/Alpha now takes into account Alpha_Type given from the parser.

Minor cleaning.

merged

more on the paper

Removed some warnings.

merge

Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.

merged

more on the paper

simplification

merge

Describe 'nominal_datatype2'.

Fixed renamings.

merged

Removed remaining cheats + some cleaning.

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.