| Sun, 27 Dec 2009 23:33:10 +0100 |
Christian Urban |
added a functor that allows checking what is added to the theorem lists
|
changeset |
files
|
| Sat, 26 Dec 2009 23:20:46 +0100 |
Christian Urban |
corrected wrong [quot_respect] attribute; tuned
|
changeset |
files
|
| Sat, 26 Dec 2009 21:36:20 +0100 |
Christian Urban |
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
|
changeset |
files
|
| Sat, 26 Dec 2009 20:45:37 +0100 |
Christian Urban |
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
|
changeset |
files
|
| Sat, 26 Dec 2009 20:24:53 +0100 |
Christian Urban |
as expected problems occure when lifting concat lemmas
|
changeset |
files
|
| Sat, 26 Dec 2009 09:03:35 +0100 |
Christian Urban |
tuned
|
changeset |
files
|
| Sat, 26 Dec 2009 08:06:45 +0100 |
Christian Urban |
commeted the absrep function
|
changeset |
files
|
| Sat, 26 Dec 2009 07:15:30 +0100 |
Christian Urban |
generalised absrep function; needs consolidation
|
changeset |
files
|
| Fri, 25 Dec 2009 00:58:06 +0100 |
Christian Urban |
tuned
|
changeset |
files
|
| Fri, 25 Dec 2009 00:17:55 +0100 |
Christian Urban |
added sanity checks for quotient_type
|
changeset |
files
|
| Thu, 24 Dec 2009 22:28:19 +0100 |
Christian Urban |
made the quotient_type definition more like typedef; now type variables need to be explicitly given
|
changeset |
files
|
| Thu, 24 Dec 2009 00:58:50 +0100 |
Christian Urban |
used Local_Theory.declaration for storing quotdata
|
changeset |
files
|
| Wed, 23 Dec 2009 23:53:03 +0100 |
Christian Urban |
tuning
|
changeset |
files
|
| Wed, 23 Dec 2009 23:22:02 +0100 |
Christian Urban |
renamed some fields in the info records
|
changeset |
files
|
| Wed, 23 Dec 2009 22:42:30 +0100 |
Christian Urban |
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
|
changeset |
files
|