wenzelm [Tue, 13 Dec 2005 19:32:05 +0100] rev 18398
tuned proofs;
wenzelm [Tue, 13 Dec 2005 19:32:04 +0100] rev 18397
added HOL/Library/Coinductive_List.thy;
urbanc [Tue, 13 Dec 2005 18:11:21 +0100] rev 18396
added a fresh_left lemma that contains all instantiation
for the various atom-types.
urbanc [Tue, 13 Dec 2005 16:30:50 +0100] rev 18395
initial commit (not to be seen by the public)
chaieb [Tue, 13 Dec 2005 16:25:10 +0100] rev 18394
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb [Tue, 13 Dec 2005 16:24:12 +0100] rev 18393
deals with Suc in mod expressions
wenzelm [Tue, 13 Dec 2005 15:46:41 +0100] rev 18392
Poplog/pml provides a proper print function already!
paulson [Tue, 13 Dec 2005 15:34:21 +0100] rev 18391
meson no longer does these examples
paulson [Tue, 13 Dec 2005 15:34:02 +0100] rev 18390
now generates the name "append"
paulson [Tue, 13 Dec 2005 15:27:43 +0100] rev 18389
removal of functional reflexivity axioms