| Fri, 27 Sep 2002 13:24:29 +0200 | paulson | Isar experiments, etc. | changeset | files |
| Fri, 27 Sep 2002 10:36:21 +0200 | paulson | Tidied. New Pi-theorem. | changeset | files |
| Fri, 27 Sep 2002 10:35:10 +0200 | paulson | new Ring example | changeset | files |
| Fri, 27 Sep 2002 10:35:01 +0200 | paulson | Isar proof | changeset | files |
| Fri, 27 Sep 2002 10:34:05 +0200 | paulson | Modules theory added | changeset | files |
| Fri, 27 Sep 2002 10:33:47 +0200 | paulson | New theory GroupTheory/Module.thy of modules | changeset | files |
| Thu, 26 Sep 2002 15:21:38 +0200 | paulson | Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML | changeset | files |
| Thu, 26 Sep 2002 10:56:20 +0200 | paulson | GroupTheory and FuncSet | changeset | files |
| Thu, 26 Sep 2002 10:51:58 +0200 | paulson | new theory for Pi-sets, restrict, etc. | changeset | files |
| Thu, 26 Sep 2002 10:51:29 +0200 | paulson | Converted Fun to Isar style. | changeset | files |
| Thu, 26 Sep 2002 10:43:43 +0200 | paulson | new document directory for GroupTheory | changeset | files |
| Thu, 26 Sep 2002 10:40:13 +0200 | paulson | converted to Isar and using new "implicit structures" instead of Sigma, etc | changeset | files |
| Wed, 25 Sep 2002 11:23:26 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 25 Sep 2002 11:22:28 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 25 Sep 2002 11:06:34 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 25 Sep 2002 07:57:36 +0200 | nipkow | Int.thy -> int.thy | changeset | files |
| Wed, 25 Sep 2002 07:55:56 +0200 | nipkow | became int.ML | changeset | files |
| Wed, 25 Sep 2002 07:54:33 +0200 | nipkow | conversion to Isar | changeset | files |
| Wed, 25 Sep 2002 07:52:07 +0200 | nipkow | converted to Isar | changeset | files |
| Wed, 25 Sep 2002 07:42:24 +0200 | nipkow | added nat_split | changeset | files |
| Sat, 21 Sep 2002 21:10:34 +0200 | paulson | converted to Isar script | changeset | files |
| Fri, 20 Sep 2002 11:49:38 +0200 | paulson | shortened a proof | changeset | files |
| Fri, 20 Sep 2002 11:49:06 +0200 | paulson | got rid of deepen_tac | changeset | files |
| Fri, 20 Sep 2002 11:48:35 +0200 | paulson | less use of x-symbols | changeset | files |
| Thu, 19 Sep 2002 16:09:16 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 19 Sep 2002 16:01:29 +0200 | nipkow | drule: added nRS | changeset | files |
| Thu, 19 Sep 2002 16:00:27 +0200 | nipkow | preserve names of rewrite rules when transforming them | changeset | files |
| Wed, 18 Sep 2002 18:19:43 +0200 | kleing | comments + usage | changeset | files |
| Wed, 11 Sep 2002 16:55:37 +0200 | paulson | Streamlined proofs of instances of Separation | changeset | files |
| Wed, 11 Sep 2002 16:53:59 +0200 | paulson | Bound variable preservation in Collect_cong | changeset | files |