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/Ex/Foo2.thy
2011-07-05
Christian Urban
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
file
|
diff
|
annotate
2010-12-28
Christian Urban
automated all strong induction lemmas
file
|
diff
|
annotate
2010-12-28
Christian Urban
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
file
|
diff
|
annotate
2010-12-26
Christian Urban
generated goals for strong induction theorems.
file
|
diff
|
annotate
2010-12-23
Christian Urban
moved all strong_exhaust code to nominal_dt_quot; tuned examples
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-14
Christian Urban
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
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
first tests about exhaust
file
|
diff
|
annotate
2010-12-08
Christian Urban
moved some code into the nominal_library
file
|
diff
|
annotate
2010-12-08
Christian Urban
kept the nested structure of constructors (belonging to one datatype)
file
|
diff
|
annotate
2010-12-07
Christian Urban
moved general theorems into the libraries
file
|
diff
|
annotate
2010-12-07
Christian Urban
automated permute_bn theorems
file
|
diff
|
annotate
less
more
(0)
-15
tip