removed dead code (nominal cannot deal with argument types of constructors that are functions)

added comment about abstraction in raw permuations

optimised the code of define_raw_perm

deleting function perm_arg in favour of the library function mk_perm

merged

tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)

FSet is a semi-lattice

merge

Putting FSet in bot typeclass.

reorder

merged

small updates to the paper; remaining points in PAPER-TODO

sub_list definition and respects

Alternate list_eq and equivalence

Some new lemmas

More cleaning

remove more metis

more metis cleaning

Getting rid of 'metis'.

merge

Remove 'defer'.

merged

tuned proofs

2 more lifted lemmas needed for second representation

Accept non-equality eqvt rules in support proofs.

merge

Locations of files in Parser

merge

minor FSet3 edits.

tuned

moved some general function into nominal_library.ML

tuned; transformation functions now take a context, a thm and return a thm

tuned

equivariance for alpha_raw in CoreHaskell is automatically derived

preliminary parser for perm_simp metod

automatic proofs for equivariance of alphas

Finished proof in Lambda.thy

merged

attempt to manual prove eqvt for alpha

Lifting in Term4.

some tuning of eqvt-infrastructure

some tuning of proofs

typo

merged

half of the pair-abs-equivalence

More on Manual/Trm4

alpha4_equivp and constant lifting.

alpha4_eqvt and alpha4_reflp

fv_eqvt in term4

Updating in Term4.

merge

Prove insert_rsp2

merged

changed header

Minor paper fixes.

temporary fix for CoreHaskell

deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell

merge

Fix the 'subscript' error.

merged

thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples

merge

merge

Separate alpha_definition.

Fix spelling in theory header

Separate define_fv.

tuned and removed dead code

moved a couple of more functions to the library

added a library for basic nominal functions; separated nominal_eqvt file

merged

first working version of the automatic equivariance procedure

Initial cleaning/reorganization in Fv.

merged

preliminary tests

deleted test

merge

merge part: delete_rsp

merge part1: none_memb_nil

added header and more tuning

more tuning

tuned

Working FSet with additional lemmas.

Much more in FSet (currently non-working)

made everything to compile

merged

some small tunings (incompleted work in Lambda.thy)

moved equivariance of map into Nominal2_Eqvt file

early ott paper

Porting lemmas from Quotient package FSet to new FSet.

added alpha-caml paper

implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _

fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _

folded changes from the conference version

added TODO item about parser creating syntax for the wrong type

corrected imports header

tuned

a few tests

added eqvt rules that are more standard

used warning instead of tracing (does not seem to produce stable output)

added small ittems about equivaraince of alpha_gens and name of lam.perm

added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed

changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac

rewrite paragraph introducing equivariance, add citation to Pitts03

edit 'contributions' section so we do not just quote directly from the reviewer

renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper

clarified comment about distinct lists in th efuture work section

tuned type-schemes example

updated (comment about weirdo example)

check whether the "weirdo" example from the binding bestiary works with shallow binders

properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)

merged

some further changes

merged

change some wording in conclusion

remove extra word

merged

added new paper directory for further work

use qualified name as string in concrete atom example

merged

simplify instance proof