| Fri, 01 Jan 2010 01:10:38 +0100 |
Christian Urban |
fixed comment errors
|
changeset |
files
|
| Fri, 01 Jan 2010 01:08:19 +0100 |
Christian Urban |
some slight tuning
|
changeset |
files
|
| Thu, 31 Dec 2009 23:53:10 +0100 |
Christian Urban |
renamed transfer to transform (Markus)
|
changeset |
files
|
| Wed, 30 Dec 2009 12:10:57 +0000 |
cu |
some small changes
|
changeset |
files
|
| 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
|