Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/Ex/Foo1.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-23
Christian Urban
test with strong inductions
file
|
diff
|
annotate
2010-12-23
Christian Urban
moved all strong_exhaust code to nominal_dt_quot; tuned examples
file
|
diff
|
annotate
2010-12-07
Christian Urban
automated permute_bn theorems
file
|
diff
|
annotate
2010-12-06
Christian Urban
automated alpha_perm_bn theorems
file
|
diff
|
annotate
2010-12-06
Christian Urban
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
file
|
diff
|
annotate
2010-11-28
Christian Urban
completed the strong exhausts rules for Foo2 using general lemmas
file
|
diff
|
annotate
2010-11-27
Christian Urban
disabled the Foo examples, because of heavy work
file
|
diff
|
annotate
2010-11-21
Christian Urban
added example Foo2.thy
file
|
diff
|
annotate
2010-11-15
Christian Urban
tuned example
file
|
diff
|
annotate
2010-11-15
Christian Urban
proved that bn functions return a finite set
file
|
diff
|
annotate
2010-11-14
Christian Urban
tuned example
file
|
diff
|
annotate
2010-11-13
Christian Urban
lifted permute_bn constants
file
|
diff
|
annotate
2010-11-13
Christian Urban
respectfulness for permute_bn functions
file
|
diff
|
annotate
2010-11-12
Christian Urban
automated permute_bn functions (raw ones first)
file
|
diff
|
annotate
2010-11-10
Christian Urban
adapted to changes by Florian on the quotient package and removed local fix for function package
file
|
diff
|
annotate
2010-09-29
Christian Urban
simplified exhaust proofs
file
|
diff
|
annotate
2010-09-29
Christian Urban
worked example Foo1 with induct_schema
file
|
diff
|
annotate
2010-09-28
Christian Urban
added Foo1 to explore a contrived example
file
|
diff
|
annotate
less
more
(0)
tip