| 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 |
| Tue, 27 Aug 2002 15:39:39 +0200 | wenzelm | removed IsarTut; | changeset | files |
| Tue, 27 Aug 2002 11:09:35 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 27 Aug 2002 11:09:33 +0200 | wenzelm | avoid duplicate fact bindings; | changeset | files |
| Tue, 27 Aug 2002 11:07:54 +0200 | wenzelm | check_file: disallow current dir (typically ""); | changeset | files |
| Tue, 27 Aug 2002 11:07:01 +0200 | wenzelm | simplified results; | changeset | files |
| Tue, 27 Aug 2002 11:06:45 +0200 | wenzelm | simplified results; | changeset | files |
| Tue, 27 Aug 2002 11:06:20 +0200 | wenzelm | Thm.proof_of; | changeset | files |
| Tue, 27 Aug 2002 11:06:07 +0200 | wenzelm | check_goal: produce error instead of warning; | changeset | files |
| Tue, 27 Aug 2002 11:05:31 +0200 | wenzelm | added proof_of; | changeset | files |
| Tue, 27 Aug 2002 11:05:13 +0200 | wenzelm | thms/axms_of_proof: proper handling of MinProof; | changeset | files |
| Tue, 27 Aug 2002 11:04:27 +0200 | wenzelm | result dependency output; | changeset | files |
| Tue, 27 Aug 2002 11:04:00 +0200 | wenzelm | dup_elim: improved error reporting; | changeset | files |
| Tue, 27 Aug 2002 11:03:05 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 27 Aug 2002 11:03:02 +0200 | wenzelm | avoid duplicate fact bindings; | changeset | files |
| Tue, 27 Aug 2002 10:59:21 +0200 | wenzelm | * Isar: preview of problems to finish 'show' now produce an error | changeset | files |
| Sat, 24 Aug 2002 18:53:43 +0200 | paulson | conversion of ZF/IntDiv to Isar script | changeset | files |