added CPS files to test (not all proofs have been completed)

added a rule about inequality of freshness between atoms to the simplifier

a simproc for simplifying Fresh when there is a sufficiently fresh atom

added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often

merged

added to the simplifier nominal_datatype.fresh lemmas

added let-eqvt back

Propagare changes from Nominal2_Base to _Exec

renamed fresh_fun to Fresh; added a simproc that deals with freshness of functions

added library routines for the constant fresh

fixed bug in simproc (also in the exec-version)

Synchronize Nominal2_Base_Exec with Nominal2_Base, equivariance for Let, avoid overloading approx twice and changes for new isabelle

improved handling in the simplifier for inequalities derived from freshness assumptions

Executing Lambda Terms

Added workaround for broken quotient_type in tip isabelle.

further cleaning

cleaned also examples

cleaned the repository for Nominal2-Isabelle2012

Created branch for Isabelle-2012

added a lemma about composition and permutations

merged

adapted to change by Markus on function.ML

Find remaining rsp theorems and provide them with the quotient definitions

Declare rsp for permute, permute_bn, alpha_bn together with their definitions instead of TrueI

merge

Pass proper rsp theorems for constructors and for size

final changes to the lmcs-paper

another iteration of the lmcs paper

moved lift_raw_const from Quotient to Nominal

updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)

slight polishing on Quotient paper

ditto

some slight polishing on the LMCS paper

merged

updated to Isabelle version April 1

a bit more on the qpaper

A recursive function over let-recs with eqvt problems

remove smt calls

More cleaning

Clean the proof of Aux

Finish all subgoals about Aux.

More on Aux

Close some of the obvious subgoals in Aux

Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.

Induction for Aux

Change definition of Aux to include alpha-convertibility for non-closed terms.

Define 'aux'

Alternate version of Nominal_Base: Executable version.

Defining nominal functions without FCB

qpaper-jv add a section about descending etc

slight tuning of Q-paper-jv

updated to new Isabelle (20 March)

updated to new Isabelle (declared keywords)

added ROOT.ML for tutorial

updated tutorial to latest version and added it to the tests

spellcheck

final changes to the lmcs paper

more one the lmcs-paper

more on the lmcs paper

merged

implemented all comments from the reviewer

slight polish of the qpaper-jv

Update to the localized quotient package

Update from Isabelle Wed Feb 15 23:19:30

added multisets to stable branch

added fs and pt for multisets

same as in function_common

qpaper-jv: merge and add to TODOs in the paper and in front.

minor

merged

added FROOT

Use the theorem by Brian, requires new Isabelle.

2 typos found by John Wickerson in QPaper

repaired all slides

tuned make-file

made all papers work again

added a session entry in order to quickly build the heap file (tests took too long)

commented out parts of TypeScheme1 in order to run all tests

updated to Isabelle 16 January

merged

added the simple fixes for the paper

added an FCB for res (will not define evry function, but is a good datapoint)

updated to explicit set type constructor (post Isabelle 3rd January)

proved that generalisation is closed under substitution

added definition for generalisation of type schemes (for paper)

added two eqvt lemmas for fset-operators

separated the two versions of type schemes into two files

added notes by referees to comment about our changes

made the paper running again

included Pi theory in tests

added file by Kirstin

merged

moved TODO into the paper

merged

some slight tuning

the default sort for type-variables in nominal specifications is fs; it is automatically addded

fixed problem with equivariance for beta_star

Reorder constructors to match Lambda

SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.

SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.

Remove transitivity from the definition of One_star and show it instead.

Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.

Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.

Update Quotient FIXME-TODO, some issues were already fixed.

Added an initial version of qpaper-jv and a TODO of things to write about.

Remove 'HERE1' and 'HERE3'.

Lift substitution of an Abstraction for BetaCR :)

Tuned renaming

Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.

Disproved the property described as 'Tzevelakos'.

partially localised the parsing process using functions fron Datatype

updated

updated in stable branch

updated all examples in stable branch

deleted Manual directory in stable branch

cleaned examples for stable branch

cleaned all papers from the stable branch

cleaned Attic in stable branch

backported no_eqvt changeset 1afcbaf4242b

Started Nominal2-Isabelle2011-1 branch and backported changeset 32abaea424bd