| Tue, 23 Feb 2010 12:49:45 +0100 |
Cezary Kaliszyk |
Looking at proving the rsp rules automatically.
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 10:06:02 +0100 |
Cezary Kaliszyk |
Main renaming + fixes for new Isabelle in IntEx2.
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 21:39:40 +0100 |
Christian Urban |
removed dead code
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 15:43:39 +0100 |
Cezary Kaliszyk |
'exc' -> 'exn' and more name and space cleaning.
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 15:28:15 +0100 |
Cezary Kaliszyk |
More indentation, names and todo cleaning in the quotient package
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 17:58:23 +0100 |
Cezary Kaliszyk |
Quotdata_dest needed for lifting theorem translation.
|
file |
diff |
annotate
|
| Wed, 27 Jan 2010 08:41:42 +0100 |
Christian Urban |
use of equiv_relation_chk in quotient_term
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 23:51:17 +0100 |
Christian Urban |
trivial
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 15:25:24 +0100 |
Cezary Kaliszyk |
Simplified matches_typ.
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 10:51:03 +0100 |
Cezary Kaliszyk |
produce defs with lthy, like prs and ids
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 10:06:29 +0100 |
Cezary Kaliszyk |
Finished organising an efficient datastructure for qconst_info.
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 08:02:20 +0100 |
Cezary Kaliszyk |
Undid changes from symtab to termtab, since we need to lookup specialized types.
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 16:39:20 +0100 |
Christian Urban |
one more item in the list of Markus
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 15:17:36 +0100 |
Cezary Kaliszyk |
Stored Termtab for constant information.
|
file |
diff |
annotate
|
| Tue, 12 Jan 2010 16:21:42 +0100 |
Cezary Kaliszyk |
minor comment editing
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 15:13:09 +0100 |
Cezary Kaliszyk |
removed quotdata_lookup_type
|
file |
diff |
annotate
|