2010-01-21 |
Cezary Kaliszyk |
Using Bexeq_rsp, and manually lifted lemma with Ex1.
|
file |
diff |
annotate
|
2010-01-21 |
Cezary Kaliszyk |
Ex1 -> Bex1 Regularization, Preparing Exeq.
|
file |
diff |
annotate
|
2010-01-20 |
Cezary Kaliszyk |
Better error messages for non matching quantifiers.
|
file |
diff |
annotate
|
2010-01-15 |
Cezary Kaliszyk |
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
|
file |
diff |
annotate
|
2010-01-15 |
Christian Urban |
slight tuning of relation_error
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
exported absrep_const for nitpick.
|
file |
diff |
annotate
|
2010-01-14 |
Cezary Kaliszyk |
Simplified matches_typ.
|
file |
diff |
annotate
|
2010-01-13 |
Cezary Kaliszyk |
Moved the matches_typ function outside a?d simplified it.
|
file |
diff |
annotate
|
2010-01-13 |
Cezary Kaliszyk |
Put relation_error as a separate function.
|
file |
diff |
annotate
|
2010-01-13 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-01-13 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-01-12 |
Christian Urban |
absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
|
file |
diff |
annotate
|
2010-01-12 |
Cezary Kaliszyk |
More indenting, bracket removing and comment restructuring.
|
file |
diff |
annotate
|
2010-01-12 |
Cezary Kaliszyk |
modifying comments/indentation in quotient_term.ml
|
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-11 |
Christian Urban |
tuned previous commit further
|
file |
diff |
annotate
|
2010-01-10 |
Christian Urban |
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
|
file |
diff |
annotate
|
2010-01-09 |
Christian Urban |
introduced separate match function
|
file |
diff |
annotate
|
2010-01-09 |
Christian Urban |
removed obsolete equiv_relation and rnamed new_equiv_relation
|
file |
diff |
annotate
|
2010-01-08 |
Cezary Kaliszyk |
New_relations, all works again including concat examples.
|
file |
diff |
annotate
|
2010-01-08 |
Cezary Kaliszyk |
Modifications for new_equiv_rel, part2
|
file |
diff |
annotate
|
2010-01-08 |
Cezary Kaliszyk |
Modifictaions for new_relation.
|
file |
diff |
annotate
|
2010-01-05 |
Christian Urban |
proper handling of error messages (code copy - maybe this can be avoided)
|
file |
diff |
annotate
|
2010-01-05 |
Christian Urban |
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
|
file |
diff |
annotate
|
2010-01-01 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-01-01 |
Christian Urban |
a slight change to abs/rep generation
|
file |
diff |
annotate
|
2010-01-01 |
Christian Urban |
fixed comment errors
|
file |
diff |
annotate
|
2010-01-01 |
Christian Urban |
some slight tuning
|
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 |
corrected wrong [quot_respect] attribute; tuned
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
commeted the absrep function
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
generalised absrep function; needs consolidation
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
used Local_Theory.declaration for storing quotdata
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
tuning
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
renamed some fields in the info records
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
cleaed a bit function mk_typedef_main
|
file |
diff |
annotate
|
2009-12-23 |
Christian Urban |
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
|
file |
diff |
annotate
|
2009-12-22 |
Christian Urban |
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
|
file |
diff |
annotate
|
2009-12-22 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-22 |
Christian Urban |
moved get_fun into quotient_term; this simplifies the overall including structure of the package
|
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 |
small tuning
|
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 |
moved the QuotMain code into two ML-files
|
file |
diff |
annotate
|