nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -50 -30 +30 +50 +100 +300 +1000 +3000 tip

First theorem with quantifiers. Learned how to use sledgehammer.
2009-10-02, by Cezary Kaliszyk
simplified the storage of the map-functions by using TheoryDataFun
2009-10-01, by Christian Urban
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
2009-09-30, by Cezary Kaliszyk
used new cong_tac
2009-09-29, by Christian Urban
First version of handling of the universal quantifier
2009-09-29, by Cezary Kaliszyk
Handling abstraction correctly.
2009-09-29, by Cezary Kaliszyk
second test
2009-09-29, by Cezary Kaliszyk
Test line
2009-09-29, by Cezary Kaliszyk
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
2009-09-29, by Cezary Kaliszyk
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
2009-09-29, by Cezary Kaliszyk
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
2009-09-29, by Cezary Kaliszyk
Merged
2009-09-29, by Cezary Kaliszyk
added name to prove
2009-09-28, by Christian Urban
consistent state
2009-09-28, by Christian Urban
some tuning of my code
2009-09-28, by Christian Urban
Cleanup
2009-09-28, by Cezary Kaliszyk
Merged
2009-09-28, by Cezary Kaliszyk
Cleaning the code with Makarius
2009-09-28, by Cezary Kaliszyk
Instnatiation with a schematic variable
2009-09-28, by Cezary Kaliszyk
added ctxt as explicit argument to build_goal; tuned
2009-09-28, by Christian Urban
slightly tuned the comment for unlam
2009-09-25, by Christian Urban
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
2009-09-25, by Christian Urban
tuned slightly one proof
2009-09-25, by Christian Urban
A version of the tactic that exports variables correctly.
2009-09-25, by Cezary Kaliszyk
Minor cleaning: whitespace, commas etc.
2009-09-25, by Cezary Kaliszyk
Correctly handling abstractions while building goals
2009-09-24, by Cezary Kaliszyk
Minor cleanup
2009-09-24, by Cezary Kaliszyk
Found the source for the exception and added a handle for it.
2009-09-24, by Cezary Kaliszyk
Make the tactic use Trueprop_cong and atomize.
2009-09-24, by Cezary Kaliszyk
Proper code for getting the prop out of the theorem.
2009-09-23, by Cezary Kaliszyk

less more | (0) -50 -30 +30 +50 +100 +300 +1000 +3000 tip

nominal2