added reference to E. Gunter's work

typos in paper

separated general nominal theory into separate folder

added README and moved examples into separate directory

merged pearl paper with this repository; started litrature subdirectory

submitted version (just in time ;o)

first complete version (slightly less than 3h more to go)

tuned

tuned strong ind section

polished infrastruct section

completed lifting section

more on the lifting section

more on the strong induction section

completed conclusion

merged

merged

updated related work section

fv_fv_bn

Update fv_bn definition for bindings allowed in types for which bn is present.

fv_perm_bn

Minor formula fixes.

fixed alpha_bn

current state

merged

added alpha_bn definition

hfill for right aligning single table cells.

Cleaning the strong induction example.

minor

Fighting with space in displaying strong induction...

starting strong induction

General paper minor fixes.

Forgot to save before commit.

Let with multiple bindings.

Fill the space below the figure.

last commit for now.

more on the conclusion

completed related work section

more on the paper

added an item about alpha-equivalence (the existential should be closer to the abstraction)

polished everything up to TODO

merged

added alpha-definition for ~~ty

permute_bn

abbreviations for \<otimes> and \<oplus>

merged

a test with let having multiple bodies

polished and removed tys from bn-functions.

merge

More on paper

started to polish alpha-equivalence section, but needs more work

started with a related work section

polished and added an example for fvars

cleaned up the section about fv's

tuned beginning of section 4

More on section 5.

More on section 5.

merged

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