Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-300
-100
-60
+60
+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.
abs_rep as ==
2009-12-04, by Cezary Kaliszyk
Cleaning the Quotients file
2009-12-04, by Cezary Kaliszyk
Minor renames and moving
2009-12-04, by Cezary Kaliszyk
Cleaning/review of QuotScript.
2009-12-04, by Cezary Kaliszyk
More cleaning
2009-12-04, by Cezary Kaliszyk
more name cleaning and removing
2009-12-04, by Cezary Kaliszyk
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning & Renaming coming from QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning in Quotients
2009-12-04, by Cezary Kaliszyk
Even more name changes and cleaning
2009-12-04, by Cezary Kaliszyk
More code cleaning and name changes
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Cezary Kaliszyk
smaller theory footprint
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
merge
2009-12-04, by Christian Urban
smaller theory footprint
2009-12-04, by Christian Urban
More name changes
2009-12-04, by Cezary Kaliszyk
Naming changes
2009-12-04, by Cezary Kaliszyk
code cleaning and renaming
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Removed previous inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
some tuning
2009-12-04, by Christian Urban
merge
2009-12-04, by Cezary Kaliszyk
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
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03, by Christian Urban
removed quot argument...not all examples work anymore
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
first version of internalised quotient theorems; added FIXME-TODO
2009-12-03, by Christian Urban
further dead code
2009-12-03, by Christian Urban
Reintroduced varifyT; we still need it for permutation definition.
2009-12-03, by Cezary Kaliszyk
Updated the examples
2009-12-03, by Cezary Kaliszyk
Fixed previous mistake
2009-12-03, by Cezary Kaliszyk
defs used automatically by clean_tac
2009-12-03, by Cezary Kaliszyk
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
2009-12-03, by Cezary Kaliszyk
Added the definition to quotient constant data.
2009-12-03, by Cezary Kaliszyk
removing unused code
2009-12-03, by Cezary Kaliszyk
merged
2009-12-03, by Christian Urban
deleted some dead code
2009-12-03, by Christian Urban
Included all_prs and ex_prs in the lambda_prs conversion.
2009-12-03, by Cezary Kaliszyk
further simplification
2009-12-03, by Christian Urban
simplified lambda_prs_conv
2009-12-03, by Christian Urban
deleted now obsolete argument rty everywhere
2009-12-02, by Christian Urban
deleted tests at the beginning of QuotMain
2009-12-02, by Christian Urban
Experiments with OPTION_map
2009-12-02, by Cezary Kaliszyk
less
more
|
(0)
-300
-100
-60
+60
+100
+300
+1000
tip