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.
simple cases for string rule inductions
2011-01-03, by Christian Urban
changed res keyword to set+ for restrictions; comment by a referee
2010-12-31, by Christian Urban
added proper case names for all induct and exhaust theorems
2010-12-31, by Christian Urban
added small example for strong inductions; functions still need a sorry
2010-12-31, by Christian Urban
removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-30, by Christian Urban
automated all strong induction lemmas
2010-12-28, by Christian Urban
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-28, by Christian Urban
generated goals for strong induction theorems.
2010-12-26, by Christian Urban
test with strong inductions
2010-12-23, by Christian Urban
moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23, by Christian Urban
moved generic functions into nominal_library
2010-12-23, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
tuned examples
2010-12-22, by Christian Urban
added fold_right which produces the correct term for left-infix operators
2010-12-22, by Christian Urban
updated to Isabelle 22 December
2010-12-22, by Christian Urban
a bit tuning
2010-12-22, by Christian Urban
corrected premises of strong exhausts theorems
2010-12-22, by Christian Urban
properly exported strong exhaust theorem; cleaned up some examples
2010-12-22, by Christian Urban
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-21, by Christian Urban
one interesting case done
2010-12-19, by Christian Urban
a stronger statement for at_set_avoiding
2010-12-19, by Christian Urban
tuned
2010-12-17, by Christian Urban
tuned
2010-12-17, by Christian Urban
simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-16, by Christian Urban
added theorem-rewriter conversion
2010-12-16, by Christian Urban
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-14, by Christian Urban
created strong_exhausts terms
2010-12-12, by Christian Urban
moved setify and listify functions into the library; introduced versions that have a type argument
2010-12-12, by Christian Urban
updated
2010-12-10, by Christian Urban
a bit more tuning of the paper
2010-12-09, by Christian Urban
brought the paper to 20 pages plus one page appendix
2010-12-09, by Christian Urban
first tests about exhaust
2010-12-08, by Christian Urban
moved some code into the nominal_library
2010-12-08, by Christian Urban
moved definition of raw bn-functions into nominal_dt_rawfuns
2010-12-08, by Christian Urban
kept the nested structure of constructors (belonging to one datatype)
2010-12-08, by Christian Urban
moved general theorems into the libraries
2010-12-07, by Christian Urban
automated permute_bn theorems
2010-12-07, by Christian Urban
updated to changes in Isabelle
2010-12-07, by Christian Urban
deleted nominal_dt_supp.ML
2010-12-06, by Christian Urban
moved code from nominal_dt_supp to nominal_dt_quot
2010-12-06, by Christian Urban
automated alpha_perm_bn theorems
2010-12-06, by Christian Urban
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-12-06, by Christian Urban
updated to Isabelle 2nd December
2010-12-03, by Christian Urban
isarfied some of the high-level proofs
2010-11-29, by Christian Urban
added abs_rename_res lemma
2010-11-29, by Christian Urban
completed proofs in Foo2
2010-11-29, by Christian Urban
completed the strong exhausts rules for Foo2 using general lemmas
2010-11-28, by Christian Urban
tuned proof to reduce number of warnings
2010-11-27, by Christian Urban
disabled the Foo examples, because of heavy work
2010-11-27, by Christian Urban
slightly simplified the Foo2 tests and hint at a general lemma
2010-11-26, by Christian Urban
completely different method fro deriving the exhaust lemma
2010-11-26, by Christian Urban
merged
2010-11-26, by Christian Urban
merged
2010-11-25, by Christian Urban
added example from the F-ing paper by Rossberg, Russo and Dreyer
2010-11-24, by Christian Urban
implemented concrete suggestion of 3rd reviewer
2010-11-24, by Christian Urban
missing freshness assumptions
2010-11-26, by Cezary Kaliszyk
foo2 strong induction
2010-11-25, by Cezary Kaliszyk
foo2 full exhausts
2010-11-24, by Cezary Kaliszyk
Foo2 strong_exhaust for first variable.
2010-11-24, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
tip