Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-300
-100
-50
-28
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
QuotMain.thy
2009-12-04
Cezary Kaliszyk
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Cleaning & Renaming coming from QuotList
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Even more name changes and cleaning
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
More code cleaning and name changes
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
More name changes
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
code cleaning and renaming
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
merge
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Removed previous inj_repabs_tac
file
|
diff
|
annotate
2009-12-04
Christian Urban
some tuning
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
merge
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
file
|
diff
|
annotate
2009-12-04
Christian Urban
merged
file
|
diff
|
annotate
2009-12-04
Christian Urban
merged
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
compose_tac instead of rtac to avoid unification; some code cleaning.
file
|
diff
|
annotate
2009-12-04
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.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Using APPLY_RSP1; again a little bit faster.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Fixes after big merge.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
The big merge; probably non-functional.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Testing the new tactic everywhere
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
First version of the deterministic rep-abs-inj-tac.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Changing = to \<equiv> in case if we want to use simp.
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
merge
file
|
diff
|
annotate
2009-12-04
Cezary Kaliszyk
Made your version work again with LIST_REL_EQ.
file
|
diff
|
annotate
2009-12-03
Christian Urban
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
file
|
diff
|
annotate
2009-12-03
Christian Urban
removed quot argument...not all examples work anymore
file
|
diff
|
annotate
2009-12-03
Christian Urban
merged
file
|
diff
|
annotate
less
more
(0)
-300
-100
-50
-28
tip