2010-01-27 |
Christian Urban |
use of equiv_relation_chk in quotient_term
|
file |
diff |
annotate
|
2010-01-14 |
Christian Urban |
trivial
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
Simplified matches_typ.
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
produce defs with lthy, like prs and ids
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
Finished organising an efficient datastructure for qconst_info.
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
Undid changes from symtab to termtab, since we need to lookup specialized types.
|
file |
diff |
annotate
|
2010-01-13 |
Christian Urban |
one more item in the list of Markus
|
file |
diff |
annotate
|
2010-01-13 |
Cezary Kaliszyk |
Stored Termtab for constant information.
|
file |
diff |
annotate
|
2010-01-12 |
Cezary Kaliszyk |
minor comment editing
|
file |
diff |
annotate
|
2010-01-11 |
Cezary Kaliszyk |
removed quotdata_lookup_type
|
file |
diff |
annotate
|
2010-01-11 |
Cezary Kaliszyk |
Fix for testing matching constants in regularize.
|
file |
diff |
annotate
|
2010-01-02 |
Christian Urban |
added a warning to the quotient_type definition, if a map function is missing
|
file |
diff |
annotate
|
2009-12-31 |
Christian Urban |
renamed transfer to transform (Markus)
|
file |
diff |
annotate
|
2009-12-30 |
cu |
some small changes
|
file |
diff |
annotate
|
2009-12-27 |
Christian Urban |
added a functor that allows checking what is added to the theorem lists
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
used Local_Theory.declaration for storing quotdata
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
renamed some fields in the info records
|
file |
diff |
annotate
|
2009-12-22 |
Christian Urban |
added "Highest Priority" category; and tuned slightly code
|
file |
diff |
annotate
|
2009-12-22 |
Christian Urban |
added a print_maps command; updated the keyword file accordingly
|
file |
diff |
annotate
|
2009-12-19 |
Christian Urban |
avoided global "open"s - replaced by local "open"s
|
file |
diff |
annotate
|
2009-12-19 |
Christian Urban |
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
|
file |
diff |
annotate
|
2009-12-17 |
Christian Urban |
minor cleaning
|
file |
diff |
annotate
|
2009-12-15 |
Christian Urban |
some commenting
|
file |
diff |
annotate
|
2009-12-10 |
Christian Urban |
added maps-printout and tuned some comments
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
more proofs in IntEx2
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Exception handling.
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
properly set up the prs_rules
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
changed names of attributes
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
added a thm list for ids
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
removed a fixme: map_info is now checked
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
final move
|
file |
diff |
annotate
| base
|