Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-300
-100
-15
+15
+100
+300
+1000
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.
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04, by Cezary Kaliszyk
compose_tac instead of rtac to avoid unification; some code cleaning.
2009-12-04, by Cezary Kaliszyk
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
2009-12-04, by Cezary Kaliszyk
Using APPLY_RSP1; again a little bit faster.
2009-12-04, by Cezary Kaliszyk
Fixes after big merge.
2009-12-04, by Cezary Kaliszyk
The big merge; probably non-functional.
2009-12-04, by Cezary Kaliszyk
Testing the new tactic everywhere
2009-12-04, by Cezary Kaliszyk
First version of the deterministic rep-abs-inj-tac.
2009-12-04, by Cezary Kaliszyk
Changing = to \<equiv> in case if we want to use simp.
2009-12-04, by Cezary Kaliszyk
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Made your version work again with LIST_REL_EQ.
2009-12-04, by Cezary Kaliszyk
less
more
|
(0)
-300
-100
-15
+15
+100
+300
+1000
tip