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.
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
more on the slides
2011-03-30, by Christian Urban
tuned IsaMakefile
2011-03-30, by Christian Urban
rearranged directories and updated to new Isabelle
2011-03-29, by Christian Urban
precise path to LaTeXsugar
2011-03-16, by Christian Urban
a lit bit more on the pearl-jv paper
2011-03-16, by Christian Urban
ported changes from function package....needs Isabelle 16 March or above
2011-03-16, by Christian Urban
more on the pearl paper
2011-03-15, by Christian Urban
equivariance for All and Ex can be proved in terms of their definition
2011-03-14, by Christian Urban
more on the paper
2011-03-11, by Christian Urban
merged
2011-03-08, by Christian Urban
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
tip