2012-03-30 Cezary Kaliszyk Clean the proof of Aux
2012-03-30 Cezary Kaliszyk Finish all subgoals about Aux.
2012-03-30 Cezary Kaliszyk More on Aux
2012-03-30 Cezary Kaliszyk Close some of the obvious subgoals in Aux
2012-03-30 Cezary Kaliszyk Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.
2012-03-29 Cezary Kaliszyk Induction for Aux
2012-03-29 Cezary Kaliszyk Change definition of Aux to include alpha-convertibility for non-closed terms.
2012-03-27 Cezary Kaliszyk Define 'aux'
2012-03-26 Cezary Kaliszyk Alternate version of Nominal_Base: Executable version.
2012-03-26 Cezary Kaliszyk Defining nominal functions without FCB
2012-03-26 Cezary Kaliszyk qpaper-jv add a section about descending etc
2012-03-21 Christian Urban slight tuning of Q-paper-jv
2012-03-20 Christian Urban updated to new Isabelle (20 March)
2012-03-17 Christian Urban updated to new Isabelle (declared keywords)
2012-03-14 Christian Urban added ROOT.ML for tutorial
2012-03-05 Christian Urban updated tutorial to latest version and added it to the tests
2012-02-29 Christian Urban spellcheck
2012-02-29 Christian Urban final changes to the lmcs paper
2012-02-29 Christian Urban more one the lmcs-paper
2012-02-29 Christian Urban more on the lmcs paper
2012-02-29 Christian Urban merged
2012-02-29 Christian Urban implemented all comments from the reviewer
2012-02-22 Christian Urban slight polish of the qpaper-jv
2012-02-28 Cezary Kaliszyk Update to the localized quotient package
2012-02-17 Cezary Kaliszyk Update from Isabelle Wed Feb 15 23:19:30
2012-02-17 Christian Urban added multisets to stable branch Nominal2-Isabelle2011-1
2012-02-17 Christian Urban added fs and pt for multisets
2012-02-16 Christian Urban same as in function_common
2012-02-09 Cezary Kaliszyk qpaper-jv: merge and add to TODOs in the paper and in front.
2012-02-09 Cezary Kaliszyk minor
2012-02-03 Christian Urban merged
2012-02-03 Christian Urban added FROOT
2012-02-03 Cezary Kaliszyk Use the theorem by Brian, requires new Isabelle.
2012-01-31 Christian Urban 2 typos found by John Wickerson in QPaper
2012-01-24 Christian Urban repaired all slides
2012-01-24 Christian Urban tuned make-file
2012-01-24 Christian Urban made all papers work again
2012-01-24 Christian Urban added a session entry in order to quickly build the heap file (tests took too long)
2012-01-16 Christian Urban commented out parts of TypeScheme1 in order to run all tests
2012-01-16 Christian Urban updated to Isabelle 16 January
2012-01-09 Christian Urban merged
2012-01-09 Christian Urban added the simple fixes for the paper
2012-01-04 Christian Urban added an FCB for res (will not define evry function, but is a good datapoint)
2012-01-03 Christian Urban updated to explicit set type constructor (post Isabelle 3rd January)
2012-01-03 Christian Urban proved that generalisation is closed under substitution
2012-01-02 Christian Urban added definition for generalisation of type schemes (for paper)
2011-12-29 Christian Urban added two eqvt lemmas for fset-operators
2011-12-29 Christian Urban separated the two versions of type schemes into two files
2011-12-29 Christian Urban added notes by referees to comment about our changes
2011-12-29 Christian Urban made the paper running again
2011-12-23 Christian Urban included Pi theory in tests
2011-12-23 Christian Urban added file by Kirstin
2011-12-22 Christian Urban merged
2011-12-22 Christian Urban moved TODO into the paper
2011-12-22 Christian Urban merged
2011-12-22 Christian Urban some slight tuning
2011-12-22 Christian Urban the default sort for type-variables in nominal specifications is fs; it is automatically addded
2011-12-22 Christian Urban fixed problem with equivariance for beta_star
2011-12-21 Cezary Kaliszyk Reorder constructors to match Lambda
2011-12-21 Cezary Kaliszyk SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.
(0) -3000 -1000 -300 -100 -60 +60 tip