2011-09-06 Christian Urban more on the lmcs paper
2011-08-28 Christian Urban updated to Isabelle 28 Aug
2011-08-19 Cezary Kaliszyk Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
2011-08-19 Cezary Kaliszyk Add lmcs-paper to hgignore
2011-08-19 Cezary Kaliszyk Add 'no-brackets' to avoid '[| |]' in papers.
2011-08-19 Cezary Kaliszyk Comment out examples with 'True' that do not work because function still does not work
2011-08-19 Cezary Kaliszyk Update to new Isabelle
2011-08-18 Christian Urban a bit more on the paper
2011-08-17 Christian Urban made same changes as in main branch
2011-08-17 Christian Urban more on the lmcs paper
2011-08-17 Christian Urban a little tuning on the paper
2011-08-16 Christian Urban more on the intro and correct style-files
2011-08-15 Christian Urban uodated to new Isabelle (15. Aug)
2011-08-15 Christian Urban updated for new Isabelle (11. Aug.)
2011-08-14 Christian Urban merged
2011-08-12 Christian Urban started lmcs paper (isabelle make lmcs)
2011-07-24 Cezary Kaliszyk update to 'termination (eqvt)'.
2011-07-22 Christian Urban tuned
2011-07-22 Christian Urban completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
2011-07-19 Christian Urban temporary fix
2011-07-19 Cezary Kaliszyk Add an ".hgignore" file
2011-07-19 Christian Urban merged
2011-07-19 Christian Urban merged
2011-07-19 Christian Urban merged
2011-07-19 Christian Urban added termination file
2011-07-19 Christian Urban preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
2011-07-19 Christian Urban generated the partial eqvt-theorem for functions
2011-07-18 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs
2011-07-18 Christian Urban moved eqvt for Option.map
2011-07-17 Christian Urban some tuning
2011-07-17 Christian Urban direct definition of height using bn
2011-07-17 Christian Urban defined a function directly over a nominal datatype with bn
2011-07-16 Christian Urban more one the NBE example
2011-07-15 Christian Urban some improvements to the NBE example
2011-07-13 Christian Urban slight tuning
2011-07-11 Cezary Kaliszyk use eqvt_at_perm
2011-07-11 Cezary Kaliszyk Remove copy of FCB and cleanup
2011-07-11 Cezary Kaliszyk Experiment with permuting eqvt_at
2011-07-11 Christian Urban combinators for local theories and lists
2011-07-11 Christian Urban merged
2011-07-11 Christian Urban some more experiments with let and bns
2011-07-08 Christian Urban some code refactoring
2011-07-07 Christian Urban merged
2011-07-07 Christian Urban code refactoring; introduced a record for raw_dt_info
2011-07-06 Christian Urban more on NBE
2011-07-06 Christian Urban more on the NBE function
2011-07-05 Christian Urban a little further with NBE
2011-07-05 Cezary Kaliszyk Setup eqvt_at for first goal
2011-07-05 Christian Urban attempt for NBE
2011-07-05 Christian Urban added some relatively simple examples from paper by Norrish
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2011-07-05 Christian Urban side commment for future use
2011-07-05 Christian Urban made the tests go through again
2011-07-05 Christian Urban added another example which seems difficult to define
2011-07-05 Christian Urban added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.
2011-07-05 Christian Urban merged
2011-07-05 Christian Urban all FCB lemmas
2011-07-05 Christian Urban exported various FCB-lemmas to a separate file
2011-07-05 Cezary Kaliszyk Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
2011-07-05 Cezary Kaliszyk Define a version of aux only for same binders. Completeness is fine.
(0) -1000 -300 -100 -60 +60 +100 tip