| Fri, 18 May 2007 16:13:07 +0200 | huffman | avoid using real_mult_inverse_left; cleaned up | changeset | files |
| Fri, 18 May 2007 16:11:13 +0200 | huffman | use mult_strict_mono instead of real_mult_less_mono | changeset | files |
| Fri, 18 May 2007 11:12:03 +0200 | berghofe | Fixed bug in subst causing primrec functions returning functions | changeset | files |
| Fri, 18 May 2007 09:16:57 +0200 | haftmann | dropped word_setup.ML | changeset | files |
| Thu, 17 May 2007 23:04:54 +0200 | krauss | added files | changeset | files |
| Thu, 17 May 2007 23:03:47 +0200 | krauss | updated | changeset | files |
| Thu, 17 May 2007 23:00:06 +0200 | krauss | moved lemmas to Nat.thy | changeset | files |
| Thu, 17 May 2007 22:58:53 +0200 | krauss | added induction principles for induction "backwards": P (Suc n) ==> P n | changeset | files |