| Mon, 30 Sep 2002 15:44:21 +0200 | nipkow | modified induct method | changeset | files |
| Fri, 27 Sep 2002 16:44:50 +0200 | paulson | Proof tidying | changeset | files |
| 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 |
| Tue, 10 Sep 2002 16:51:31 +0200 | paulson | renamed M_triv_axioms to M_trivial and M_axioms to M_basic | changeset | files |
| Tue, 10 Sep 2002 16:47:17 +0200 | paulson | tweaks | changeset | files |
| Mon, 09 Sep 2002 17:28:29 +0200 | nipkow | *** empty log message *** | changeset | files |
| Mon, 09 Sep 2002 17:07:12 +0200 | nipkow | bug in counter example finder | changeset | files |
| Sat, 07 Sep 2002 22:04:28 +0200 | paulson | conversion of ZF/Integ/{Int,Bin} to Isar scripts | changeset | files |
| Thu, 05 Sep 2002 14:03:03 +0200 | paulson | added checking so that (rename_tac "x y") is rejected, since | changeset | files |
| Tue, 03 Sep 2002 18:49:30 +0200 | paulson | tidied | changeset | files |
| Tue, 03 Sep 2002 18:49:10 +0200 | paulson | deleted redundant material (quasiformula, ...) and rationalized | changeset | files |
| Tue, 03 Sep 2002 18:43:15 +0200 | paulson | fixed the typesetting | changeset | files |
| Tue, 03 Sep 2002 13:41:29 +0200 | nipkow | *** empty log message *** | changeset | files |
| Mon, 02 Sep 2002 12:25:19 +0200 | paulson | Added missing rewrite rule and some arith examples | changeset | files |
| Mon, 02 Sep 2002 11:07:26 +0200 | nipkow | order_less_irrefl: [simp] -> [iff] | changeset | files |
| Sun, 01 Sep 2002 19:39:25 +0200 | nipkow | *** empty log message *** | changeset | files |
| Sat, 31 Aug 2002 14:03:49 +0200 | paulson | converted Hyperreal/Zorn to Isar format and moved to Library | changeset | files |
| Fri, 30 Aug 2002 16:42:45 +0200 | paulson | removal of blast.overloaded | changeset | files |
| Thu, 29 Aug 2002 16:15:11 +0200 | wenzelm | updated; | changeset | files |
| Thu, 29 Aug 2002 16:08:32 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 29 Aug 2002 16:08:30 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 29 Aug 2002 11:15:36 +0200 | paulson | fixed a name clash | changeset | files |
| Wed, 28 Aug 2002 15:27:43 +0200 | wenzelm | improved tell_thm_deps; | changeset | files |
| Wed, 28 Aug 2002 13:08:50 +0200 | paulson | various new lemmas for Constructible | changeset | files |
| Wed, 28 Aug 2002 13:08:34 +0200 | paulson | completion of the consistency proof for AC | changeset | files |
| Tue, 27 Aug 2002 17:25:44 +0200 | wenzelm | thms_containing: allow "_" in specification; | changeset | files |
| Tue, 27 Aug 2002 17:24:41 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 27 Aug 2002 16:41:52 +0200 | wenzelm | * Pure: disallow duplicate fact bindings within new-style theory files; | changeset | files |
| Tue, 27 Aug 2002 16:41:01 +0200 | wenzelm | disallow duplicate fact bindings for drafts (i.e. within new-style theory files); | changeset | files |
| Tue, 27 Aug 2002 15:40:58 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 27 Aug 2002 15:40:33 +0200 | wenzelm | avoid duplicate fact bindings; | changeset | files |