| Tue, 05 Jan 2010 14:23:45 +0100 |
Christian Urban |
proper handling of error messages (code copy - maybe this can be avoided)
|
file |
diff |
annotate
|
| Tue, 05 Jan 2010 14:09:04 +0100 |
Christian Urban |
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 23:59:32 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 11:30:00 +0100 |
Christian Urban |
a slight change to abs/rep generation
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 01:10:38 +0100 |
Christian Urban |
fixed comment errors
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 01:08:19 +0100 |
Christian Urban |
some slight tuning
|
file |
diff |
annotate
|
| Sun, 27 Dec 2009 23:33:10 +0100 |
Christian Urban |
added a functor that allows checking what is added to the theorem lists
|
file |
diff |
annotate
|
| Sat, 26 Dec 2009 23:20:46 +0100 |
Christian Urban |
corrected wrong [quot_respect] attribute; tuned
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sat, 26 Dec 2009 09:03:35 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Sat, 26 Dec 2009 08:06:45 +0100 |
Christian Urban |
commeted the absrep function
|
file |
diff |
annotate
|
| Sat, 26 Dec 2009 07:15:30 +0100 |
Christian Urban |
generalised absrep function; needs consolidation
|
file |
diff |
annotate
|
| Thu, 24 Dec 2009 00:58:50 +0100 |
Christian Urban |
used Local_Theory.declaration for storing quotdata
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 23:53:03 +0100 |
Christian Urban |
tuning
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 23:22:02 +0100 |
Christian Urban |
renamed some fields in the info records
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 21:30:23 +0100 |
Christian Urban |
cleaed a bit function mk_typedef_main
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 10:31:54 +0100 |
Christian Urban |
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
|
file |
diff |
annotate
|
| Tue, 22 Dec 2009 21:31:44 +0100 |
Christian Urban |
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
|
file |
diff |
annotate
|
| Tue, 22 Dec 2009 21:16:11 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Tue, 22 Dec 2009 21:06:46 +0100 |
Christian Urban |
moved get_fun into quotient_term; this simplifies the overall including structure of the package
|
file |
diff |
annotate
|
| Sat, 19 Dec 2009 22:21:51 +0100 |
Christian Urban |
avoided global "open"s - replaced by local "open"s
|
file |
diff |
annotate
|
| Sat, 19 Dec 2009 22:09:57 +0100 |
Christian Urban |
small tuning
|
file |
diff |
annotate
|
| Sat, 19 Dec 2009 22:04:34 +0100 |
Christian Urban |
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 14:58:33 +0100 |
Christian Urban |
moved the QuotMain code into two ML-files
|
file |
diff |
annotate
|