2010-02-10 Cezary Kaliszyk merge
2010-02-10 Cezary Kaliszyk Fixed rbv6, when translating to OTT.
2010-02-10 Cezary Kaliszyk Some cleaning of proofs.
2010-02-10 Christian Urban merged again
2010-02-10 Christian Urban merged
2010-02-10 Cezary Kaliszyk more minor space and bracket modifications.
2010-02-10 Cezary Kaliszyk More changes according to the standards.
2010-02-10 Cezary Kaliszyk A concrete example, with a proof that rbv is not regular and
2010-02-09 Christian Urban proper declaration of types and terms during parsing (removes the varifyT when storing data)
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban slight correction
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More about trm6
2010-02-09 Christian Urban merged
2010-02-09 Cezary Kaliszyk the specifications of the respects.
2010-02-09 Cezary Kaliszyk trm6 with the 'Foo' constructor.
2010-02-09 Cezary Kaliszyk removing unnecessary brackets
2010-02-09 Cezary Kaliszyk More indentation cleaning.
2010-02-09 Cezary Kaliszyk 'exc' -> 'exn' and more name and space cleaning.
2010-02-09 Cezary Kaliszyk Fully qualified exception names.
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
2010-02-09 Christian Urban minor tuning
2010-02-09 Cezary Kaliszyk Explicitly marked what is bound.
2010-02-09 Cezary Kaliszyk Cleaning and updating in Terms.
2010-02-09 Cezary Kaliszyk Looking at the trm2 example
2010-02-09 Cezary Kaliszyk Fixed pattern matching, now the test in Abs works correctly.
2010-02-08 Christian Urban added a test case
2010-02-08 Christian Urban merged
2010-02-08 Christian Urban moved some lemmas to Nominal; updated all files
2010-02-08 Cezary Kaliszyk merge
2010-02-08 Cezary Kaliszyk Comments.
2010-02-08 Christian Urban slightly tuned
2010-02-08 Cezary Kaliszyk Proper context fixes lifting inside instantiations.
2010-02-08 Cezary Kaliszyk Fixed the context import/export and simplified LFex.
2010-02-08 Christian Urban added 2 papers about core haskell
2010-02-07 Christian Urban fixed lemma name
2010-02-07 Christian Urban updated to latest Nominal2
2010-02-06 Christian Urban minor
2010-02-06 Christian Urban some tuning
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk Fixes for Bex1 removal.
2010-02-05 Cezary Kaliszyk Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
2010-02-05 Cezary Kaliszyk A procedure that properly instantiates the types too.
2010-02-05 Cezary Kaliszyk More code abstracted away
2010-02-05 Cezary Kaliszyk A bit more intelligent and cleaner code.
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk A proper version of the attribute
2010-02-05 Christian Urban merged
2010-02-05 Christian Urban eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
2010-02-04 Cezary Kaliszyk The automatic lifting translation function, still with dummy types,
2010-02-04 Cezary Kaliszyk Quotdata_dest needed for lifting theorem translation.
2010-02-04 Christian Urban fixed (permute_eqvt in eqvts makes this simpset always looping)
2010-02-04 Christian Urban rollback of the test
2010-02-04 Christian Urban linked versions - instead of copies
2010-02-04 Christian Urban merged
2010-02-04 Christian Urban restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
2010-02-03 Cezary Kaliszyk More let-rec experiments
2010-02-03 Christian Urban proposal for an alpha equivalence
2010-02-03 Cezary Kaliszyk Lets different.
2010-02-03 Cezary Kaliszyk Simplified the proof.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban proved that bv for lists respects alpha for terms
2010-02-03 Cezary Kaliszyk Finished remains on the let proof.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Lets are ok.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added type-scheme example
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Definitions for trm5
2010-02-03 Christian Urban another adaptation for the eqvt-change
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban fixed proofs that broke because of eqvt
2010-02-03 Cezary Kaliszyk Minor fix.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk alpha5 pseudo-injective
2010-02-03 Christian Urban fixed proofs in Abs.thy
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added a first eqvt_tac which pushes permutations inside terms
2010-02-03 Cezary Kaliszyk The alpha-equivalence relation for let-rec. Not sure if correct...
2010-02-03 Cezary Kaliszyk Starting with a let-rec example.
2010-02-03 Cezary Kaliszyk Minor
2010-02-03 Cezary Kaliszyk Some cleaning and eqvt proof
2010-02-03 Cezary Kaliszyk The trm1_support lemma explicitly and stated a strong induction principle.
2010-02-03 Cezary Kaliszyk More ingredients in Terms.
2010-02-02 Cezary Kaliszyk Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
2010-02-02 Cezary Kaliszyk More in Terms
2010-02-02 Cezary Kaliszyk First experiments in Terms.
2010-02-02 Cezary Kaliszyk LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
2010-02-02 Cezary Kaliszyk Disambiguating the syntax.
2010-02-02 Cezary Kaliszyk Minor uncommited changes from LamEx2.
2010-02-02 Cezary Kaliszyk Some equivariance machinery that comes useful in LF.
2010-02-02 Cezary Kaliszyk Generalized the eqvt proof for single binders.
2010-02-02 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
2010-02-02 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction.
2010-02-02 Cezary Kaliszyk With unfolding Rep/Abs_eqvt no longer needed.
2010-02-02 Cezary Kaliszyk Lam2 finished apart from Rep_eqvt.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk All should be ok now.
2010-02-01 Christian Urban repaired according to changes in Abs.thy
2010-02-01 Christian Urban added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
2010-02-01 Christian Urban cleaned
2010-02-01 Christian Urban updated from huffman
2010-02-01 Christian Urban updated from nominal-huffman
2010-02-01 Cezary Kaliszyk Fixed wrong rename.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk Lambda based on alpha_gen, under construction.
2010-02-01 Christian Urban updated from huffman - repo
2010-02-01 Christian Urban renamed Abst/abst to Abs/abs
2010-02-01 Christian Urban got rid of RAbst type - is now just pairs
2010-02-01 Cezary Kaliszyk Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01 Cezary Kaliszyk The current state of fv vs supp proofs in LF.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Christian Urban merged
2010-02-01 Christian Urban slight tuning
2010-02-01 Christian Urban renamed function according to the name of the constant
(0) -1000 -120 +120 +1000 tip