Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-30
-10
-7
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Quot/Examples/IntEx.thy
Thu, 21 Jan 2010 09:55:05 +0100
Cezary Kaliszyk
Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
file
|
diff
|
annotate
Thu, 14 Jan 2010 15:25:24 +0100
Cezary Kaliszyk
Simplified matches_typ.
file
|
diff
|
annotate
Wed, 13 Jan 2010 13:12:04 +0100
Cezary Kaliszyk
Removed the 'oops' in IntEx.
file
|
diff
|
annotate
Wed, 13 Jan 2010 00:46:31 +0100
Christian Urban
tuned
file
|
diff
|
annotate
Wed, 13 Jan 2010 00:45:28 +0100
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
Mon, 11 Jan 2010 11:51:19 +0100
Cezary Kaliszyk
Fix for testing matching constants in regularize.
file
|
diff
|
annotate
Mon, 11 Jan 2010 00:31:29 +0100
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
less
more
(0)
-30
-10
-7
tip