Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+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.
introduced a general procedure for structural inductions; simplified reflexivity proof
2010-09-20, by Christian Urban
updated to Isabelle Sept 16
2010-09-18, by Christian Urban
updated to Isabelle Sept 13
2010-09-18, by Christian Urban
tuned code
2010-09-12, by Christian Urban
tuned (to conform with indentation policy of Markus)
2010-09-11, by Christian Urban
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-09-10, by Christian Urban
generated inducts rule by Project_Rule.projections
2010-09-05, by Christian Urban
added the definition supp_rel (support w.r.t. a relation)
2010-09-05, by Christian Urban
merged
2010-09-04, by Christian Urban
got rid of Nominal2_Supp (is now in Nomina2_Base)
2010-09-04, by Christian Urban
moved everything out of Nominal_Supp
2010-09-04, by Christian Urban
renamed alpha_gen -> alpha_set and Abs -> Abs_set etc
2010-09-04, by Christian Urban
moved a proof to Abs
2010-09-04, by Christian Urban
got rid of Nominal_Atoms (folded into Nominal2_Base)
2010-09-04, by Christian Urban
cleaned a bit various thy-files in Nominal-General
2010-09-04, by Christian Urban
adapted paper to changes
2010-09-03, by Christian Urban
made the fv-definition aggree more with alpha (needed in the support proofs)
2010-09-03, by Christian Urban
removed lemma finite_set (already in simpset)
2010-09-03, by Christian Urban
added supp_set lemma
2010-09-03, by Christian Urban
some experiments with support
2010-09-02, by Christian Urban
added eqvt-attribute for permute_abs lemmas
2010-09-02, by Christian Urban
slides of my talk
2010-08-31, by Christian Urban
merge
2010-08-30, by Cezary Kaliszyk
update qpaper to new isabelle
2010-08-30, by Cezary Kaliszyk
No need to unfold mem_def with rsp/prs (requires new isabelle).
2010-08-30, by Cezary Kaliszyk
Anonymize, change Quotient to Quot and fix indentation
2010-08-30, by Cezary Kaliszyk
renamed NewParser to Nominal2
2010-08-29, by Christian Urban
tuned
2010-08-29, by Christian Urban
updated todos
2010-08-29, by Christian Urban
added fs-instance proofs
2010-08-29, by Christian Urban
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+100
+300
tip