Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-100
-60
+60
+100
+300
+1000
+3000
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.
Merge
2009-10-24, by cek
Finally lifted induction, with some manually added simplification lemmas.
2009-10-24, by Cezary Kaliszyk
changed encoding from utf8 to ISO8 (needed to work with xemacs)
2009-10-24, by Christian Urban
Merge
2009-10-24, by cek
Preparing infrastructire for LAMBDA_PRS
2009-10-24, by Cezary Kaliszyk
moved the map_funs setup into QuotMain
2009-10-24, by Christian Urban
Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24, by Cezary Kaliszyk
More infrastructure for automatic lifting of theorems lifted before
2009-10-24, by Cezary Kaliszyk
More infrastructure for automatic lifting of theorems lifted before
2009-10-24, by Cezary Kaliszyk
Undid wrong merge
2009-10-24, by cek
Tried rolling back
2009-10-24, by cek
Cleaning the mess
2009-10-24, by cek
Merge
2009-10-24, by cek
Better tactic and simplified the proof further
2009-10-24, by cek
fixed problem with incorrect ABS/REP name
2009-10-24, by Christian Urban
Stronger tactic, simpler proof.
2009-10-23, by Cezary Kaliszyk
Split Finite Set example into separate file
2009-10-23, by Cezary Kaliszyk
eqsubst_tac
2009-10-23, by Cezary Kaliszyk
Trying to get a simpler lemma with the whole infrastructure
2009-10-23, by Cezary Kaliszyk
Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-23, by Cezary Kaliszyk
Further developing the tactic and simplifying the proof
2009-10-22, by Cezary Kaliszyk
res_forall_rsp_tac further simplifies the proof
2009-10-22, by Cezary Kaliszyk
Working on the proof and the tactic.
2009-10-22, by Cezary Kaliszyk
The proof gets simplified
2009-10-22, by Cezary Kaliszyk
Removed an assumption
2009-10-22, by Cezary Kaliszyk
The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22, by Cezary Kaliszyk
The problems with 'abs' term.
2009-10-22, by Cezary Kaliszyk
Simplified the proof with some tactic... Still hangs sometimes.
2009-10-22, by Cezary Kaliszyk
More proof
2009-10-22, by Cezary Kaliszyk
Got rid of instantiations in the proof
2009-10-22, by Cezary Kaliszyk
Removed some debugging messages
2009-10-22, by Cezary Kaliszyk
tuned and attempted to store data about the quotients (does not work yet)
2009-10-22, by Christian Urban
tuned
2009-10-22, by Christian Urban
slight tuning
2009-10-22, by Christian Urban
fixed my_reg
2009-10-21, by Christian Urban
Reorganization of the construction part
2009-10-21, by Cezary Kaliszyk
Simplified proof more
2009-10-21, by Cezary Kaliszyk
Cleaning the code
2009-10-21, by Cezary Kaliszyk
Further reorganization
2009-10-21, by Cezary Kaliszyk
Further reorganizing the file
2009-10-21, by Cezary Kaliszyk
Reordering
2009-10-21, by Cezary Kaliszyk
cterm_instantiate also fails for some strange reason...
2009-10-21, by Cezary Kaliszyk
preparing arguments for res_inst_tac
2009-10-21, by Cezary Kaliszyk
Trying res_inst_tac
2009-10-21, by Cezary Kaliszyk
started to write code for storing data about the quotients
2009-10-20, by Christian Urban
some minor tuning
2009-10-20, by Christian Urban
tuned and fixed the earlier fix
2009-10-20, by Christian Urban
fixed the abs case in my_reg and added an app case
2009-10-20, by Christian Urban
my version of regularise (still needs to be completed)
2009-10-20, by Christian Urban
moved the map-info and fun-info section to quotient.ML
2009-10-20, by Christian Urban
Test if we can already do sth with the transformed theorem.
2009-10-18, by Cezary Kaliszyk
slight fix and tuning
2009-10-18, by Christian Urban
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
2009-10-18, by Christian Urban
Partial simplification of the proof
2009-10-17, by Cezary Kaliszyk
Some QUOTIENTS
2009-10-17, by Cezary Kaliszyk
Only QUOTIENSs are left to fnish proof
2009-10-17, by Cezary Kaliszyk
More higher order unification problems
2009-10-17, by Cezary Kaliszyk
Merged
2009-10-17, by Cezary Kaliszyk
Simplified
2009-10-17, by Cezary Kaliszyk
Further in the proof
2009-10-17, by Cezary Kaliszyk
less
more
|
(0)
-100
-60
+60
+100
+300
+1000
+3000
tip