Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-15
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Quot/QuotMain.thy
2010-01-26
Cezary Kaliszyk
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
file
|
diff
|
annotate
2010-01-26
Cezary Kaliszyk
All eq_reflections apart from the one of 'id_apply' can be removed.
file
|
diff
|
annotate
2010-01-25
Christian Urban
ids *cannot* be object equalities
file
|
diff
|
annotate
2010-01-25
Christian Urban
renamed QuotScript to QuotBase
file
|
diff
|
annotate
2010-01-25
Christian Urban
cleaned some theorems
file
|
diff
|
annotate
2010-01-21
Cezary Kaliszyk
Automatic injection of Bexeq
file
|
diff
|
annotate
2010-01-21
Cezary Kaliszyk
Using Bexeq_rsp, and manually lifted lemma with Ex1.
file
|
diff
|
annotate
2010-01-21
Cezary Kaliszyk
The missing rule.
file
|
diff
|
annotate
2010-01-16
Christian Urban
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
file
|
diff
|
annotate
2010-01-14
Cezary Kaliszyk
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
file
|
diff
|
annotate
2010-01-14
Cezary Kaliszyk
Finished organising an efficient datastructure for qconst_info.
file
|
diff
|
annotate
2010-01-12
Christian Urban
absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
file
|
diff
|
annotate
2010-01-11
Christian Urban
tuned previous commit further
file
|
diff
|
annotate
2010-01-10
Christian Urban
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
file
|
diff
|
annotate
2010-01-08
Cezary Kaliszyk
Modifictaions for new_relation.
file
|
diff
|
annotate
less
more
(0)
-15
tip