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.
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
compose_tac works with the full instantiation.
2009-10-17, by Cezary Kaliszyk
slightly simplified get_fun function
2009-10-17, by Christian Urban
The instantiated version is the same modulo beta
2009-10-17, by Cezary Kaliszyk
Fully manually instantiated. Still fails...
2009-10-17, by Cezary Kaliszyk
Little progress with match/instantiate
2009-10-17, by Cezary Kaliszyk
Fighting with the instantiation
2009-10-16, by Cezary Kaliszyk
Symmetric version of REP_ABS_RSP
2009-10-16, by Cezary Kaliszyk
Progressing with the proof
2009-10-16, by Cezary Kaliszyk
Finally fix get_fun.
2009-10-16, by Cezary Kaliszyk
A fix for one fun_map; doesn't work for more.
2009-10-16, by Cezary Kaliszyk
fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-16, by Christian Urban
Description of the problem with get_fun.
2009-10-15, by Cezary Kaliszyk
A proper build_goal_term function.
2009-10-15, by Cezary Kaliszyk
Cleaning the code
2009-10-15, by Cezary Kaliszyk
Merged
2009-10-15, by Cezary Kaliszyk
Cleaning the proofs
2009-10-15, by Cezary Kaliszyk
Cleaning the code, part 4
2009-10-15, by Cezary Kaliszyk
slightly improved tyRel
2009-10-15, by Christian Urban
Reordering the code, part 3
2009-10-15, by Cezary Kaliszyk
Reordering the code, part 2.
2009-10-15, by Cezary Kaliszyk
Reordering the code, part 1.
2009-10-15, by Cezary Kaliszyk
Minor cleaning.
2009-10-15, by Cezary Kaliszyk
The definition of Fold1
2009-10-15, by Cezary Kaliszyk
A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-15, by Cezary Kaliszyk
Proving the proper RepAbs version
2009-10-14, by Cezary Kaliszyk
Forgot to save, second part of the commit
2009-10-14, by Cezary Kaliszyk
Manually regularized list_induct2
2009-10-14, by Cezary Kaliszyk
less
more
|
(0)
-100
-60
+60
+100
+300
+1000
+3000
tip