| Tue, 05 Sep 2000 18:48:22 +0200 | wenzelm | added not_const; | changeset | files |
| Tue, 05 Sep 2000 18:48:04 +0200 | wenzelm | improved recdef setup; | changeset | files |
| Tue, 05 Sep 2000 18:47:46 +0200 | wenzelm | lemmas [recdef_cong] = map_cong; | changeset | files |
| Tue, 05 Sep 2000 18:47:27 +0200 | wenzelm | removed Add_recdef_congs [map_cong] (see Main.thy); | changeset | files |
| Tue, 05 Sep 2000 18:47:03 +0200 | wenzelm | tuned setup; | changeset | files |
| Tue, 05 Sep 2000 18:46:36 +0200 | wenzelm | iff declarations moved to clasimp.ML; | changeset | files |
| Tue, 05 Sep 2000 18:45:51 +0200 | wenzelm | added not; | changeset | files |
| Tue, 05 Sep 2000 18:45:09 +0200 | wenzelm | simplified PG/X-Symbol intro; | changeset | files |
| Tue, 05 Sep 2000 18:44:42 +0200 | wenzelm | recdef hints (attributes and modifiers); | changeset | files |
| Tue, 05 Sep 2000 18:43:54 +0200 | wenzelm | added 'iff' modifier; | changeset | files |
| Tue, 05 Sep 2000 18:43:22 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 05 Sep 2000 18:43:05 +0200 | wenzelm | updated; | changeset | files |
| Tue, 05 Sep 2000 13:53:39 +0200 | nipkow | *** empty log message *** | changeset | files |
| Tue, 05 Sep 2000 13:12:00 +0200 | paulson | tidied, proving gcd_greatest_iff and using induct_tac | changeset | files |