Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
removed dead code
2011-06-02, by Christian Urban
finished the missing obligations
2011-06-02, by Cezary Kaliszyk
merged
2011-06-02, by Christian Urban
a test with a recursion combinator defined on top of nominal_primrec
2011-06-02, by Christian Urban
Use FCB to simplify proof
2011-06-02, by Cezary Kaliszyk
merge
2011-06-02, by Cezary Kaliszyk
Remove SMT
2011-06-02, by Cezary Kaliszyk
hopefully final fix for ho-functions
2011-06-01, by Christian Urban
first test to fix the problem with free variables
2011-06-01, by Christian Urban
proved subst for All constructor in type schemes.
2011-06-01, by Cezary Kaliszyk
DB translation using index; easier to reason about.
2011-06-01, by Cezary Kaliszyk
Problem: free variables in the goal
2011-06-01, by Cezary Kaliszyk
fixed previous commit
2011-06-01, by Cezary Kaliszyk
equivariance of db_trans
2011-06-01, by Cezary Kaliszyk
fixed the problem with cps-like functions
2011-05-31, by Christian Urban
DeBruijn translation in a simplifier friendly way
2011-05-31, by Cezary Kaliszyk
map_term can be defined when equivariance is assumed
2011-05-31, by Cezary Kaliszyk
map_term is not a function the way it is defined
2011-05-31, by Cezary Kaliszyk
Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
2011-05-31, by Cezary Kaliszyk
Simple eqvt proofs with perm_simps for clarity
2011-05-31, by Cezary Kaliszyk
tuned last commit
2011-05-31, by Christian Urban
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-05-31, by Christian Urban
updated to new Isabelle
2011-05-26, by Christian Urban
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
2011-05-25, by Christian Urban
more on slides
2011-05-24, by Christian Urban
added slides for copenhagen
2011-05-22, by Christian Urban
added a problem with inductive_cases (reported by Randy)
2011-05-14, by Christian Urban
misc
2011-05-13, by Christian Urban
made the subtyping work again
2011-05-10, by Christian Urban
updated to new Isabelle (> 9 May)
2011-05-10, by Christian Urban
merged
2011-05-09, by Christian Urban
added two mutual recursive inductive definitions
2011-05-03, by Christian Urban
deleted two functions from the API
2011-05-03, by Christian Urban
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
2011-05-03, by Christian Urban
more on pearl-paper
2011-05-09, by Christian Urban
more on pearl-paper
2011-05-04, by Christian Urban
updated Quotient paper so that it compiles again
2011-05-02, by Christian Urban
merged
2011-04-28, by Christian Urban
added slides for beijing
2011-04-28, by Christian Urban
more to the pearl paper
2011-04-22, by Christian Urban
updated to snapshot Isabelle 19 April
2011-04-19, by Christian Urban
merged
2011-04-18, by Christian Urban
added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
2011-04-18, by Christian Urban
New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
2011-04-15, by Cezary Kaliszyk
merged
2011-04-13, by Christian Urban
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-04-13, by Christian Urban
shanghai slides
2011-04-12, by Christian Urban
pictures for slides
2011-04-11, by Christian Urban
Shanghai slides
2011-04-11, by Christian Urban
more paper
2011-04-10, by Christian Urban
eqvt of supp and fresh is proved using equivariance infrastructure
2011-04-10, by Christian Urban
more paper
2011-04-10, by Christian Urban
more on the paper
2011-04-09, by Christian Urban
tuned paper
2011-04-09, by Christian Urban
tuned paper
2011-04-09, by Christian Urban
typo
2011-04-09, by Christian Urban
more on paper
2011-04-08, by Christian Urban
eqvt_lambda without eta-expansion
2011-04-08, by Christian Urban
changed default preprocessor that does not catch variables only occuring on the right
2011-04-06, by Christian Urban
final version of slides
2011-03-31, by Christian Urban
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
tip