Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-50
-30
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
2009-12-24
Christian Urban
tuned
file
|
diff
|
annotate
2009-12-23
Christian Urban
renamed QUOT_TYPE to Quot_Type
file
|
diff
|
annotate
2009-12-22
Christian Urban
moved get_fun into quotient_term; this simplifies the overall including structure of the package
file
|
diff
|
annotate
2009-12-22
Christian Urban
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
file
|
diff
|
annotate
2009-12-21
Christian Urban
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
file
|
diff
|
annotate
2009-12-17
Christian Urban
minor cleaning
file
|
diff
|
annotate
2009-12-17
Christian Urban
moved the QuotMain code into two ML-files
file
|
diff
|
annotate
2009-12-15
Cezary Kaliszyk
lambda_prs & solve_quotient_assum cleaned.
file
|
diff
|
annotate
2009-12-15
Christian Urban
some commenting
file
|
diff
|
annotate
2009-12-14
Cezary Kaliszyk
Fixed previous commit.
file
|
diff
|
annotate
2009-12-14
Cezary Kaliszyk
Moved DETERM inside Repeat & added SOLVE around quotient_tac.
file
|
diff
|
annotate
2009-12-14
Cezary Kaliszyk
reply to question in code
file
|
diff
|
annotate
2009-12-14
Cezary Kaliszyk
Reply in code.
file
|
diff
|
annotate
2009-12-13
Christian Urban
a few code annotations
file
|
diff
|
annotate
2009-12-13
Christian Urban
another pass on apply_rsp
file
|
diff
|
annotate
less
more
(0)
-50
-30
tip