Hi Gerwin, > Is anyone prepared to leak Florian's new email address so I may haunt him?
I am prepared to be haunted ;-), I am still on the users and dev mailing list and will follow them following the walrus strategy (only dive up instantly if you think it is necessary). First, a quick and dirty answer to your question: > haftmann@scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ hg cat -r > 14cabf5fa710 . | grep -oP '^(lemmas?|corollary|theorems?) [A-Za-z0-9_'\'']+' > | sort > names1.txt > haftmann@scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ hg cat -r > 56e3520b68b2 . | grep -oP '^(lemmas?|corollary|theorems?) [A-Za-z0-9_'\'']+' > | sort > names2.txt > haftmann@scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ diff names1.txt > names2.txt > 197c197 > < lemma bl_and_mask > --- >> lemma bl_and_mask' > 663d662 > < lemma shiftl_0 > 676a676 >> lemma shiftl_x_0 > 679d678 > < lemma shiftr_0 > 689a689 >> lemma shiftr_x_0 > 1037d1036 > < lemmas unat_sub > 1228d1226 > < lemma uint_0 > 1237a1236 >> lemma uint_eq_0 > 1276d1274 > < lemma unat_sub_simple > 1341d1338 > < lemma word_less_sub1 > 1344d1340 > < lemma word_le_sub1 These should be the only lemma names affected. I must confess that the changeset I have produced there really does not follow best Isabelle practice. So it is not clear to me whether these have been mere slips or intentional skips due to duplication. But giving the quick and dirty queries from above it should not be too difficult to reassure what case applies. Is this enough to help to solve your problem? Otherwise I will keep on tracking this, but this might take a while. > Someone (Florian, I guess) thought it was a good idea to have "one unified > Word theory" as the commit log says. I heartily disagree, but whatever. The motiviation for this changeset in the first place were the repeated pleas for adding code generation to the word type. Examining what was needed lead me to the conclusion that the previous division of the Word theories was largely artificial, in particular the very ancient practice to separate definitions from their corresponding lemmas into different theories. For me it was beyond doubt that a theory defining the word type should be called "Word", but this was already in use for the main entrance point, so I was also reluctant to further partition that unified Word theory. With some irony you could call this an instance of aspect-oriented programming: it is difficult to weave the aspect of code generation into a theory where it is beyond your scope what the original intentions have been. What always made me stumble is that parts of the Word theories (in particular Bit_Int) are so highly dependent on the accidental representation of int values as signed binary numerals; I always asked myself whether this modelling is really necessary or could be formulated in a more abstract fashion. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev