Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-15
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/nominal_dt_rawfuns.ML
2011-04-13
Christian Urban
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
file
|
diff
|
annotate
2010-12-28
Christian Urban
automated all strong induction lemmas
file
|
diff
|
annotate
2010-12-21
Christian Urban
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
file
|
diff
|
annotate
2010-12-16
Christian Urban
simple cases for strong inducts done; infrastructure for the difficult ones is there
file
|
diff
|
annotate
2010-12-12
Christian Urban
created strong_exhausts terms
file
|
diff
|
annotate
2010-12-12
Christian Urban
moved setify and listify functions into the library; introduced versions that have a type argument
file
|
diff
|
annotate
2010-12-08
Christian Urban
moved definition of raw bn-functions into nominal_dt_rawfuns
file
|
diff
|
annotate
2010-12-07
Christian Urban
automated permute_bn theorems
file
|
diff
|
annotate
2010-11-15
Christian Urban
proved that bn functions return a finite set
file
|
diff
|
annotate
2010-11-15
Christian Urban
fixed bug in fv function where a shallow binder binds lists of names
file
|
diff
|
annotate
2010-11-12
Christian Urban
automated permute_bn functions (raw ones first)
file
|
diff
|
annotate
2010-10-17
Christian Urban
all tests work again
file
|
diff
|
annotate
2010-10-14
Christian Urban
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
file
|
diff
|
annotate
2010-09-10
Christian Urban
tuned (to conform with indentation policy of Markus)
file
|
diff
|
annotate
2010-09-03
Christian Urban
made the fv-definition aggree more with alpha (needed in the support proofs)
file
|
diff
|
annotate
less
more
(0)
-15
tip