| 2009-12-11 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
deleted struct_match by Pattern.match (fixes a problem in LarryInt)
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
FSet3 minor fixes + cases
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
added Int example from Larry
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
Added FSet3 with a formalisation of finite sets based on Michael's one.
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
Updated TODO list together.
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
Merge
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
More theorem renaming.
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
Renamed theorems in IntEx2 to conform to names in Int.
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
Updated comments.
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
renamed Larrys example
|
changeset |
files
|
| 2009-12-11 |
Cezary Kaliszyk |
New syntax for definitions.
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
changed error message
|
changeset |
files
|
| 2009-12-11 |
Christian Urban |
reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
slightly tuned
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
added maps-printout and tuned some comments
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Option and Sum quotients.
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Regularized the hard lemma.
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Simplification of Babses for regularize; will probably become injection
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Found the problem with ttt3.
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
minor
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Moved Unused part of locale to Unused QuotMain.
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
more tuning
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
simplified the instantiation of QUOT_TRUE in procedure_tac
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
completed previous commit
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
deleted DT/NDT diagnostic code
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
moved the interpretation code into Unused.thy
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
added an attempt to get a finite set theory
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
removed memb and used standard mem (member from List.thy)
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
simplified proofs
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
removed quot_respect attribute of a non-standard lemma
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-10 |
Christian Urban |
naming in this file cannot be made to agree to the original (PROBLEM?)
|
changeset |
files
|
| 2009-12-10 |
Cezary Kaliszyk |
Lifted some kind of induction.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
more proofs in IntEx2
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Finished one proof in IntEx2.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
slightly more on IntEx2
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
proved (with a lot of pain) that times_raw is respectful
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
fixed minor stupidity
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Exception handling.
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Code cleaning.
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
foldr_rsp.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
deleted make_inst3
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
moved function and tuned comment
|
changeset |
files
|