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

polish explanation of additive group syntax

final version of the pearl paper

my final version of the paper

added an induction principle for permutations; removed add_perm construction

isarfied proof about existence of a permutation list

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.