nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -300 -100 -60 +60 +100 +300 +1000 tip

Fixed the induction problem + some more proofs.
2010-01-29, by Cezary Kaliszyk
equivariance of rfv and alpha.
2010-01-29, by Cezary Kaliszyk
Added the experiments with fun and function.
2010-01-29, by Cezary Kaliszyk
now also final step is proved - the supp of lambdas is now completely characterised
2010-01-29, by Christian Urban
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-29, by Christian Urban
improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28, by Christian Urban
merged
2010-01-28, by Christian Urban
general abstraction operator and complete characterisation of its support and freshness
2010-01-28, by Christian Urban
Ported existing part of LF to new permutations and alphas.
2010-01-28, by Cezary Kaliszyk
attempt of a general abstraction operator
2010-01-28, by Christian Urban
attempt to prove equivalence between alpha definitions
2010-01-28, by Christian Urban
End of renaming.
2010-01-28, by Cezary Kaliszyk
Minor when looking at lam.distinct and lam.inject
2010-01-28, by Cezary Kaliszyk
Renamed Bexeq to Bex1_rel
2010-01-28, by Cezary Kaliszyk
Substracting bounds from free variables.
2010-01-28, by Cezary Kaliszyk
Improper interface for datatype and function packages and proper interface lateron.
2010-01-28, by Cezary Kaliszyk
merged
2010-01-28, by Christian Urban
minor
2010-01-28, by Christian Urban
test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28, by Christian Urban
Recommited the changes for nitpick
2010-01-28, by Cezary Kaliszyk
Correct types which fixes the printing.
2010-01-27, by Cezary Kaliszyk
fv for subterms
2010-01-27, by Cezary Kaliszyk
Fix the problem with later examples. Maybe need to go back to textual specifications.
2010-01-27, by Cezary Kaliszyk
Some processing of variables in constructors to get free variables.
2010-01-27, by Cezary Kaliszyk
Parsing of the input as terms and types, and passing them as such to the function package.
2010-01-27, by Cezary Kaliszyk
Undid the parsing, as it is not possible with thy->lthy interaction.
2010-01-27, by Cezary Kaliszyk
merge
2010-01-27, by Cezary Kaliszyk
Some cleaning of thy vs lthy vs context.
2010-01-27, by Cezary Kaliszyk
merged
2010-01-27, by Christian Urban
tuned comment
2010-01-27, by Christian Urban
completely ported
2010-01-27, by Christian Urban
Another string in the specification.
2010-01-27, by Cezary Kaliszyk
Variable takes a 'name'.
2010-01-27, by Cezary Kaliszyk
merge
2010-01-27, by Cezary Kaliszyk
When commenting discovered a missing case of Babs->Abs regularization.
2010-01-27, by Cezary Kaliszyk
merged
2010-01-27, by Christian Urban
mostly ported Terms.thy to new Nominal
2010-01-27, by Christian Urban
merge
2010-01-27, by Cezary Kaliszyk
Commenting regularize
2010-01-27, by Cezary Kaliszyk
very rough example file for how nominal2 specification can be parsed
2010-01-27, by Christian Urban
reordered cases in regularize (will be merged into two cases)
2010-01-27, by Christian Urban
use of equiv_relation_chk in quotient_term
2010-01-27, by Christian Urban
some slight tuning
2010-01-27, by Christian Urban
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
2010-01-27, by Christian Urban
added another example with indirect recursion over lists
2010-01-27, by Christian Urban
just moved obsolete material into Attic
2010-01-26, by Christian Urban
added an LamEx example together with the new nominal infrastructure
2010-01-26, by Christian Urban
Bex1_Bexeq_regular.
2010-01-26, by Cezary Kaliszyk
Hom Theorem with exists unique
2010-01-26, by Cezary Kaliszyk
2 cases for regularize with split, lemmas with split now lift.
2010-01-26, by Cezary Kaliszyk
Simpler statement that has the problem.
2010-01-26, by Cezary Kaliszyk
Found a term that does not regularize.
2010-01-26, by Cezary Kaliszyk
A triple is still ok.
2010-01-26, by Cezary Kaliszyk
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
2010-01-26, by Cezary Kaliszyk
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
2010-01-26, by Cezary Kaliszyk
Sigma cleaning works with split_prs (still manual proof).
2010-01-26, by Cezary Kaliszyk
tuned
2010-01-26, by Christian Urban
merged
2010-01-26, by Christian Urban
cleaning of QuotProd; a little cleaning of QuotList
2010-01-26, by Christian Urban
added prs and rsp lemmas for Inl and Inr
2010-01-26, by Christian Urban

less more | (0) -300 -100 -60 +60 +100 +300 +1000 tip

nominal2