updated to Isabelle 2016-1

updated to Isabelle 2016-1

fixed a problem with two example theories

updated to Isabelle 2016

removed junk

updated branch

updated examples

updated for Isabelle 2015

updated for 2014 release

changed add.assoc

changed nominal_primrec to nominal_function and termination to nominal_termination

changed nominal_primrec into the more appropriate nominal_function

changes from upstream

updated changes from upstream (AFP)

some small additions to examples

updated to massive changes in Isabelle

updated to changes in Isabelle

updated to Isabelle changes

fixed bug with support and freshness lemmas not being simplified properly

updated with current AFP version

updated to changes in Isabelle

added new slides

added slides

restricted fresh_ineq simproc so that it is faster

updated to lates Isabelle

added some lemmas

updated to ne Isabelle

updated to new Isabelle

updated to simplifier changes

added example for locales (by Tjark Weber)

tuned

Fixed proofs to work with 13ab4f0a0b0e.

Various changes to support Nominal2 commands in local contexts.

Manual merge of d121bd2a5a47 from Isabelle/AFP.

tuned

reverted change in the stable branch

updated to quotient package changes (by Kuncar)

adapt to changes Isabelle/84d01fd733cf

updated for 2013 release

updated README

added Nominal2-Isabelle 2013 Branch

tuned

fixed problem with not fresh enough permutation name in nominal_primrec

adapted to latest change of Markus on the function package

updated to changes in the type-def package

removed "use" - replaced by "ML_file"

removed fork_mono flag

tuned

added a nefangled ROOT file

definition of an auxiliary graph in nominal-primrec definitions

tuned

added eqvt-lemma for function composition

added new ROOT session file

command_spec antiquotation.

added a simproc for alpha-equivalence to the simplifier

streamlined definition of alpha-equivalence for single binders (used flip instead of swap)

used ML-antiquotation command_spec for new commands

added eqvt for finfun_apply

improved the finfun parts

added finfun-type to Nominal

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

Beta: equ and equ2 are not the same relations, equ2 seems not to be beta-eta equality.

updated to lates changes in the datatype package

a bit more on alpha-beta-equated terms

generated the correct thm-list for showing that qfv are equal to support

updated to Isabelle 13 Dec

updated to Isabelle 6 Dec (thanks to Odrej Kuncar)

tiny improvement by removing one unnecessary assumption

deleted old strong_exhaust proof

tuned

silly syntax bug

updated to changes in the quotient package (patch by Ondrej Kuncar)

termination does not automatically prove equivariance for the defined function (label: no_eqvt)

a few more experiments with alpha-beta

used simproc-antiquotation

slides for talk in Leicester

updated to Isabelle 26 Nov

added eqvt-lemma for Image

proved supp for QVar; QApp still fails - probably stronger condistion is needed

added initial test about alpha-beta-equated terms

Add equivariance for alpha_lam_raw and abs_lam.

all examples work again after quotient package has been "de-localised"

updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package

final polishing?

space

spelling

added comments from Andrei

bib

more polishing

added a footnote

some minor polishing

some minor polishing

merged

some polishing

Alternate versions of alpha for finitely supported types on the raw level

merged

changes

deleted PNil

deleted PNil

Load pdfsetup and hyperref last.

Correct BIB entry

updated to Isabelle 19 Sept

more polishing

minor

polished

included comments from Ramana

polished

all material

all material

almost finished

more on paper

more on the paper

more on paper

minor

more on paper

more on paper

more on paper

more on the paper

more

more on paper

more

paper

merged

more on paper

more

more on the paper

more on paper

more on the lmcs paper

updated to Isabelle 28 Aug

Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].

Add lmcs-paper to hgignore

Add 'no-brackets' to avoid '[| |]' in papers.

Comment out examples with 'True' that do not work because function still does not work

Update to new Isabelle

a bit more on the paper

made same changes as in main branch

more on the lmcs paper

a little tuning on the paper

more on the intro and correct style-files

uodated to new Isabelle (15. Aug)

updated for new Isabelle (11. Aug.)

merged

started lmcs paper (isabelle make lmcs)

update to 'termination (eqvt)'.

tuned

completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list

temporary fix

Add an ".hgignore" file

merged

merged

merged

added termination file

preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec

generated the partial eqvt-theorem for functions

added a flag (eqvt) to termination proofs arising fron nominal_primrecs

moved eqvt for Option.map

some tuning

direct definition of height using bn

defined a function directly over a nominal datatype with bn

more one the NBE example

some improvements to the NBE example

slight tuning

use eqvt_at_perm

Remove copy of FCB and cleanup

Experiment with permuting eqvt_at

combinators for local theories and lists

merged

some more experiments with let and bns

some code refactoring

merged

code refactoring; introduced a record for raw_dt_info

more on NBE

more on the NBE function

a little further with NBE

Setup eqvt_at for first goal

attempt for NBE

added some relatively simple examples from paper by Norrish

changed bind to binds in specifications; bind will cause trouble with Monad_Syntax

side commment for future use

made the tests go through again

added another example which seems difficult to define

added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.

merged

all FCB lemmas

exported various FCB-lemmas to a separate file

Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?

Define a version of aux only for same binders. Completeness is fine.

Move If / Let with 'True' to the end of Lambda

merged

tuned

added an example that recurses over two arguments; the interesting proof-obligation is not yet done

Let with a different invariant; not true.

Add non-working Lambda_F_T using FCB2

Added non-working CPS3 using FCB2

Change CPS1 to FCB2

Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn

side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function

Exhaust Issue

clarified a sentence

more code refactoring

combined distributed data for alpha in alpha_result (partially done)

moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through

added a warning if a theorem is already declared as equivariant

merged

Prove bn injectivity and experiment more with Let

some experiments

trying new fcb in let/subst

Leftover only inj and eqvt

eapply fcb ok

Removed Inl and Inr

relaxed type in fcb

fcb with explicit bn function

added let-rec example

Experiments with res

proved the fcb also for sets (no restriction yet)

copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom

streamlined the fcb-proof and made fcb1 a special case of fcb

completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)

fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.

renamed ds to dset (disagreement set)

added small lemma about disagreement set

merge

New-style fcb for multiple binders.

equality of lst_binder and a few helper lemmas [l]lst. T = [l]lst. S <-> T = S

only one of the fcb precondistions are needed (probably the same with the perm-conditions)

another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy

did all cases, except the multiple binder case

an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders.

except for the interated binder case, finished definition in Calssical.thy

Make examples work with non-precompiled image

Remove Lambda_add.thy

The examples in Lambda_add can be defined by nominal_function directly

Theory name changes for JEdit

More usual names for substitution properties

Second Fixed Point Theorem

Speed-up the completeness proof.

the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl

added file

expanded the example

fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package

tuned

deleted some dead code

some rudimentary infrastructure for storing data about nominal datatypes

constants with the same names

Quotients/TODO addtion

Minor

merge

spelling

merge

Abs_set_fcb

function for let-rec

TODO/minor

Move lst_fcb to Nominal2_Abs

More minor TODOs

Update TODO

Let/minor

Update Quotient/TODO and remove some attic code

merge

little on cps2

got rid of the boolean flag in the raw_equivariance function

Fix

merge

CPS3 can be defined with eqvt_rhs.

moved for the moment CPS translations into the example directory

merged

added eqvt_at and invariant for boths sides of the equations

Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.

added a test that every function must be of pt-sort

all tests work again

added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method

added an abstract

added a stub for function paper; "isabelle make fnpaper"

merge

one TODO and one Problem?

merge

Some TODOs

merge

TypeSchemes work with 'default'.

tuned some proofs

fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough

tuned

Move working examples before non-working ones

Optimized proofs and removed some garbage.

merge

Slightly modify fcb for list1 and put in common place.

Experiments with Let

Eval can be defined with additional freshness

Minor simplification

abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.

More experiments with 'default'

Finished the proof with the invariant

Issue with 'default'

merged

merged

using the option "default" the function package allows one to give an explicit default value

Simpler proof of TypeSchemes/substs

Simplify fcb_res

FCB for res binding and simplified proof of subst for type schemes

Simplify ln-trans proof

cbvs can be easily defined without an invariant

defined the "count-bound-variables-occurences" function which has an accumulator like trans

merged

remove garbage (proofs that assumes the invariant outside function)

Proof of trans with invariant

Testing invariant in Lambda_F_T

cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file

fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant

slightly stronger property in fundef_ex_prop

added an option for an invariant (at the moment only a stub)

added a more general lemma fro fundef_ex1

Trying the induction on the graph

Finish and test the locale approach

FiniteSupp precondition in the function is enough to get rid of completeness obligationss

recursion combinator inside a locale

merge

F for lambda used to define translation to locally nameless

typo

removed dead code

finished the missing obligations

merged

a test with a recursion combinator defined on top of nominal_primrec

Use FCB to simplify proof

merge

Remove SMT

hopefully final fix for ho-functions

first test to fix the problem with free variables

proved subst for All constructor in type schemes.

DB translation using index; easier to reason about.

Problem: free variables in the goal

fixed previous commit

equivariance of db_trans

fixed the problem with cps-like functions

DeBruijn translation in a simplifier friendly way

map_term can be defined when equivariance is assumed

map_term is not a function the way it is defined

Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.

Simple eqvt proofs with perm_simps for clarity

tuned last commit

functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition

updated to new Isabelle

added eq_iff and distinct lemmas of nominal datatypes to the simplifier

more on slides

added slides for copenhagen

added a problem with inductive_cases (reported by Randy)

misc

made the subtyping work again

updated to new Isabelle (> 9 May)

merged

added two mutual recursive inductive definitions

deleted two functions from the API

proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)

more on pearl-paper

more on pearl-paper

updated Quotient paper so that it compiles again

merged

added slides for beijing

more to the pearl paper

updated to snapshot Isabelle 19 April

merged

added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April

New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.

merged

introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive

shanghai slides

pictures for slides

Shanghai slides

more paper

eqvt of supp and fresh is proved using equivariance infrastructure

more paper

more on the paper

tuned paper

tuned paper

typo

more on paper

eqvt_lambda without eta-expansion

changed default preprocessor that does not catch variables only occuring on the right

final version of slides

more on the slides

tuned IsaMakefile

rearranged directories and updated to new Isabelle

precise path to LaTeXsugar

a lit bit more on the pearl-jv paper

ported changes from function package....needs Isabelle 16 March or above

more on the pearl paper

equivariance for All and Ex can be proved in terms of their definition

more on the paper

merged

more on the pearl paper

distinct names at toplevel

merge

Pairing function

updated pearl papers

a bit more tuning

included old test cases for perm_simp into ROOT.ML file

split the library into a basics file; merged Nominal_Eqvt into Nominal_Base

some slight polishing

merged

added a lemma about fresh_star and Abs

Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.

typeschemes/subst

further experiments with typeschemes subst

Finished the proof of a function that invents fresh variable names.

added eqvt for length

added eqvt lemmas for filter and distinct

added eqvt for cartesian products

cleaned up the experiments so that the tests go through

merge

Experiments defining a function on Let

updated TODO

Lambda.thy which works with Nominal_Isabelle2011

merged

removed diagnostic code

Only one of the subgoals is needed

Experiments with substitution on set+

More properties that relate abs_res and abs_set. Also abs_res with less binders.

alpha_res implies alpha_set :)

Showing that the binders difference is fresh for the left side solves the goal for 'set'.

Experiments with functions

some experiments

the proofs with eqvt_at

made eqvt-proof explicit in the function definitions

merge

minor

Down as infixr

added some slides

added Tutorial6

cleaning up

merged

cleaned up Tutorial 3 with solutions

Missing val.simps

merge

Tutorial 4s

cleaned up and solution section

cleaned up tutorial1...added solution file

better version of Tutorial 1

better flow of proofs and definitions and proof

separated type preservation and progress into a separate file

substitution lemma in separate file

added unbind example

a bit tuning

first split of tutorrial theory

added a very rough version of the tutorial; all seems to work

added obtain_fresh lemma; tuned Lambda.thy

base file for the tutorial (contains definitions for heigt, subst and beta-reduction)

ported some of the old proofs to serve as testcases

added eqvt and supp lemma for removeAll (function from List.thy)

theory name as it should be

removed diagnostic code

added Minimal file to test things

defined height as a function that returns an integer

deleted diagnostic code

some tryes about substitution over type-schemes

defined properly substitution

derived stronger Abs_eq_iff2 theorems

made alpha_abs_set_stronger1 stronger

removed finiteness assumption from set_rename_perm

alpha_abs_set_stronger1

alpha_abs_let_stronger is not true in the same form

the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions

modified the renaming_perm lemmas

added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)

added a few examples of functions to Lambda.thy

exported nominal function code to external file

removed old testing code from Lambda.thy

moved high level code from LamTest into the main libraries.

eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation

subst also works now

nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions

strengthened renaming lemmas

added eqvt_lemmas for subset and psubset

a few lemmas about freshness for at and at_base

added a property about finite support in the presense of eqvt_at

instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis

solved subgoals for depth and subst function

added eqvt_at premises in function definition - however not proved at the moment

added one further lemma about equivariance of THE_default

equivariance of THE_default under the uniqueness assumption

derived equivariance for the function graph and function relation

a modified function package where, as a test, True has been injected into the compatibility condictions

removed last traces of debugging code

removed debugging code abd introduced a guarded tracing function

moved Weakening up....it does not compile when put at the last position

tuned

added weakening to the test cases

cleaned up weakening proof and added a version with finit sets

same

some further lemmas for fsets

made sure the raw datatypes and raw functions do not get any mixfix syntax

exported the code into a separate file

strong rule inductions; as an example the weakening lemma works

final version of the ESOP paper; used set+ instead of res as requested by one reviewer

file with most of the strong rule induction development

simple cases for string rule inductions

changed res keyword to set+ for restrictions; comment by a referee

added proper case names for all induct and exhaust theorems

added small example for strong inductions; functions still need a sorry

removed local fix for bug in induction_schema; added setup method for strong inductions

automated all strong induction lemmas

proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML

generated goals for strong induction theorems.

test with strong inductions

moved all strong_exhaust code to nominal_dt_quot; tuned examples

moved generic functions into nominal_library

slight tuning

slight tuning

tuned examples

added fold_right which produces the correct term for left-infix operators

updated to Isabelle 22 December

a bit tuning

corrected premises of strong exhausts theorems

properly exported strong exhaust theorem; cleaned up some examples

all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code

one interesting case done

a stronger statement for at_set_avoiding

tuned

tuned

simple cases for strong inducts done; infrastructure for the difficult ones is there

added theorem-rewriter conversion

freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)

created strong_exhausts terms

moved setify and listify functions into the library; introduced versions that have a type argument

updated

a bit more tuning of the paper

brought the paper to 20 pages plus one page appendix

first tests about exhaust

moved some code into the nominal_library

moved definition of raw bn-functions into nominal_dt_rawfuns

kept the nested structure of constructors (belonging to one datatype)

moved general theorems into the libraries

automated permute_bn theorems

updated to changes in Isabelle

deleted nominal_dt_supp.ML

moved code from nominal_dt_supp to nominal_dt_quot

automated alpha_perm_bn theorems

ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof

updated to Isabelle 2nd December

isarfied some of the high-level proofs

added abs_rename_res lemma

completed proofs in Foo2

completed the strong exhausts rules for Foo2 using general lemmas

tuned proof to reduce number of warnings

disabled the Foo examples, because of heavy work

slightly simplified the Foo2 tests and hint at a general lemma

completely different method fro deriving the exhaust lemma

merged

merged

added example from the F-ing paper by Rossberg, Russo and Dreyer

implemented concrete suggestion of 3rd reviewer

missing freshness assumptions

foo2 strong induction

foo2 full exhausts

Foo2 strong_exhaust for first variable.

single rename in let2

current isabelle

added example Foo2.thy

tuned example

proved that bn functions return a finite set

added a test for the various shallow binders

fixed bug in fv function where a shallow binder binds lists of names

merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy

deleted special Nominal2_FSet theory

moved rest of the lemmas from Nominal2_FSet to the TypeScheme example

moved most material fron Nominal2_FSet into the Nominal_Base theory

tuned example

lifted permute_bn simp rules

lifted permute_bn constants

respectfulness for permute_bn functions

automated permute_bn functions (raw ones first)

adapted to changes by Florian on the quotient package and removed local fix for function package

expanded the paper by uncommenting the comments and adding the appendix

fixed locally the problem with the function package; all tests work again

added a test about subtyping; disabled two tests, because of problem with function package

small typo

squeezed qpaper to 6 pages

Qpaper / Move examples to commented out appendix

Unanonymize qpaper

FSet changes for Qpaper

Remove FSet and use the one from Isabelle

took out comment about map-types / adapted to recent changes

use definitions instead of functions

tuned

used functions instead of definitions

added missing style file

Use the generalized compositional quotient theorem

fixed typo

all tests work again

some tuning

naming scheme is now *_fset (not f*_)

more cleaning

further tuning

renamed fminus_raw to diff_list

renamed fcard_raw to card_list

slight update

Further reorganisation and cleaning

further cleaning

typo

FSet: stronger fact in Isabelle.

FSet synchronizing

Synchronizing FSet further.

Partially merging changes from Isabelle

fixed the typo in the abstract and the problem with append (the type of map_k and map_list seems to be indeed incorrect....did not yet look at this)

changed format of the pearl paper

deleted some unused lemmas