| Thu, 08 Jul 1999 18:27:01 +0200 | wenzelm | Theorems involving oracles will be printed with a suffixed \verb|[!]|; | changeset | files |
| Thu, 08 Jul 1999 18:26:24 +0200 | wenzelm | updated usedir; | changeset | files |
| Thu, 08 Jul 1999 13:55:18 +0200 | paulson | integer division | changeset | files |
| Thu, 08 Jul 1999 13:48:11 +0200 | paulson | Renaming of theorems from _nat0 to _int0 and _nat1 to _int1 | changeset | files |
| Thu, 08 Jul 1999 13:47:27 +0200 | paulson | Introduction of integer division algorithm | changeset | files |
| Thu, 08 Jul 1999 13:46:29 +0200 | paulson | changed header to cope with default if_weak_cong | changeset | files |
| Thu, 08 Jul 1999 13:44:47 +0200 | paulson | Now if_weak_cong is a standard congruence rule | changeset | files |
| Thu, 08 Jul 1999 13:43:42 +0200 | paulson | Introduction of integer division algorithm | changeset | files |
| Thu, 08 Jul 1999 13:42:31 +0200 | paulson | tidied proofs to cope with default if_weak_cong | changeset | files |
| Thu, 08 Jul 1999 13:38:41 +0200 | paulson | Now if_weak_cong is a standard congruence rule | changeset | files |
| Thu, 08 Jul 1999 13:37:40 +0200 | paulson | new theory IntDiv.thy | changeset | files |
| Thu, 08 Jul 1999 13:35:33 +0200 | paulson | new files IntDiv.{thy,ML} | changeset | files |
| Wed, 07 Jul 1999 00:15:06 +0200 | wenzelm | tuned output; | changeset | files |
| Tue, 06 Jul 1999 21:16:29 +0200 | wenzelm | simp only: attribute, method arg; | changeset | files |
| Tue, 06 Jul 1999 21:14:34 +0200 | wenzelm | use generic numeral encoding and syntax; | changeset | files |
| Tue, 06 Jul 1999 21:13:12 +0200 | wenzelm | adapted to generic numerals; | changeset | files |
| Tue, 06 Jul 1999 21:11:34 +0200 | wenzelm | simp only; | changeset | files |
| Tue, 06 Jul 1999 21:09:23 +0200 | wenzelm | added Numeral.thy; | changeset | files |
| Tue, 06 Jul 1999 21:09:05 +0200 | wenzelm | _reflcl; | changeset | files |
| Tue, 06 Jul 1999 21:08:30 +0200 | wenzelm | added Numeral.thy, Tools/numeral_syntax.ML; | changeset | files |
| Tue, 06 Jul 1999 21:06:51 +0200 | wenzelm | removed proof history nesting commands (not useful); | changeset | files |
| Tue, 06 Jul 1999 21:06:03 +0200 | wenzelm | improved errors; | changeset | files |
| Tue, 06 Jul 1999 21:04:37 +0200 | wenzelm | removed nesting (unused); | changeset | files |
| Tue, 06 Jul 1999 21:03:57 +0200 | wenzelm | export term_of_typ; | changeset | files |
| Tue, 06 Jul 1999 21:03:34 +0200 | wenzelm | begin_theory: disallow finished; | changeset | files |
| Tue, 06 Jul 1999 21:03:03 +0200 | wenzelm | added clear_mss; | changeset | files |
| Mon, 05 Jul 1999 09:52:25 +0200 | wenzelm | variant version; | changeset | files |
| Sun, 04 Jul 1999 20:21:45 +0200 | wenzelm | fixed scope of x:??H; | changeset | files |