| Tue, 19 Feb 2002 23:49:26 +0100 | wenzelm | Paulson:1989; | changeset | files |
| Tue, 19 Feb 2002 23:45:54 +0100 | wenzelm | "isatool usedir -D output HOL Test && isatool document Test/output"; | changeset | files |
| Sat, 16 Feb 2002 21:26:19 +0100 | kleing | fixed copy_all | changeset | files |
| Sat, 16 Feb 2002 20:59:34 +0100 | wenzelm | converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy); | changeset | files |
| Fri, 15 Feb 2002 20:43:44 +0100 | wenzelm | removed unused unmask_interrupt; | changeset | files |
| Fri, 15 Feb 2002 20:43:09 +0100 | wenzelm | clarified copy_all; | changeset | files |
| Fri, 15 Feb 2002 20:42:00 +0100 | wenzelm | moved copy_all to Thy/present.ML; | changeset | files |
| Fri, 15 Feb 2002 20:41:39 +0100 | wenzelm | replaced nodups by distinct; | changeset | files |
| Fri, 15 Feb 2002 20:41:19 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 15 Feb 2002 12:07:27 +0100 | paulson | a new definition of "restrict" | changeset | files |
| Thu, 14 Feb 2002 20:30:49 +0100 | wenzelm | made MLWorks happy; | changeset | files |
| Thu, 14 Feb 2002 12:24:02 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 14 Feb 2002 12:06:07 +0100 | nipkow | nodups -> distinct | changeset | files |
| Thu, 14 Feb 2002 11:50:52 +0100 | nipkow | nodups -> distinct | changeset | files |
| Wed, 13 Feb 2002 10:48:29 +0100 | paulson | deleted some redundant 'addS*Es [equalityC*E]'s | changeset | files |
| Wed, 13 Feb 2002 10:45:08 +0100 | paulson | new function lemmas | changeset | files |
| Wed, 13 Feb 2002 10:44:39 +0100 | paulson | tidied. no more special simpset (super_ss) | changeset | files |
| Wed, 13 Feb 2002 10:44:07 +0100 | paulson | new lemmas for closure under Union | changeset | files |
| Tue, 12 Feb 2002 20:35:35 +0100 | wenzelm | eliminated Pure/Isar/comment.ML; | changeset | files |
| Tue, 12 Feb 2002 20:34:02 +0100 | wenzelm | ANTIQUOTE_FAIL; | changeset | files |
| Tue, 12 Feb 2002 20:33:37 +0100 | wenzelm | eliminated Isar/comment.ML; | changeset | files |
| Tue, 12 Feb 2002 20:33:03 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 12 Feb 2002 20:32:23 +0100 | wenzelm | added isabelle-hol-book; | changeset | files |
| Tue, 12 Feb 2002 20:31:40 +0100 | wenzelm | * Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text; | changeset | files |
| Tue, 12 Feb 2002 20:28:27 +0100 | wenzelm | got rid of explicit marginal comments (now stripped earlier from input); | changeset | files |
| Tue, 12 Feb 2002 20:25:58 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 11 Feb 2002 17:30:58 +0100 | wenzelm | ML-Systems/smlnj-compiler.ML compatibility tweak; | changeset | files |
| Mon, 11 Feb 2002 10:56:33 +0100 | wenzelm | include SVC_Test; | changeset | files |
| Thu, 07 Feb 2002 11:07:03 +0100 | berghofe | Theorems are only "pre-named" if the do not already have names. | changeset | files |
| Wed, 06 Feb 2002 14:10:35 +0100 | berghofe | Added function could_unify to speed up rewriting of proof terms. | changeset | files |
| Wed, 06 Feb 2002 14:09:55 +0100 | berghofe | Indexes of variables in expanded proofs are now incremented to avoid clashes. | changeset | files |
| Tue, 05 Feb 2002 23:18:08 +0100 | wenzelm | moved SVC stuff to ex; | changeset | files |
| Tue, 05 Feb 2002 15:51:28 +0100 | berghofe | New function maxidx_of_proof. | changeset | files |
| Mon, 04 Feb 2002 13:16:54 +0100 | paulson | New-style versions of these old examples | changeset | files |
| Sat, 02 Feb 2002 13:26:51 +0100 | berghofe | Rewrite procedure now works for both compact and full proof objects. | changeset | files |
| Wed, 30 Jan 2002 14:05:29 +0100 | wenzelm | escape_mfix; | changeset | files |
| Wed, 30 Jan 2002 14:00:36 +0100 | wenzelm | added literal; | changeset | files |
| Wed, 30 Jan 2002 14:00:25 +0100 | wenzelm | prep_mixfix': proper use of Syntax.literal; | changeset | files |
| Wed, 30 Jan 2002 13:59:57 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 30 Jan 2002 12:22:59 +0100 | paulson | mu-syntax for the LEAST operator | changeset | files |
| Wed, 30 Jan 2002 12:22:40 +0100 | paulson | Multiset: added the translation Mult(A) => A-||>nat-{0} | changeset | files |
| Mon, 28 Jan 2002 23:35:20 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 28 Jan 2002 18:51:48 +0100 | wenzelm | GPLed; | changeset | files |
| Mon, 28 Jan 2002 18:50:23 +0100 | wenzelm | tuned header; | changeset | files |
| Mon, 28 Jan 2002 18:48:25 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 28 Jan 2002 17:52:13 +0100 | schirmer | Bali added | changeset | files |
| Mon, 28 Jan 2002 17:00:19 +0100 | schirmer | Isabelle/Bali sources; | changeset | files |
| Sat, 26 Jan 2002 19:20:01 +0100 | wenzelm | Isar cases/induct: no backtracking; | changeset | files |
| Sat, 26 Jan 2002 19:17:15 +0100 | wenzelm | cases: really append cases_default; | changeset | files |
| Sat, 26 Jan 2002 19:15:51 +0100 | wenzelm | generic DETERM; | changeset | files |
| Fri, 25 Jan 2002 15:42:59 +0100 | paulson | ZF | changeset | files |
| Thu, 24 Jan 2002 22:44:10 +0100 | wenzelm | copy_files *.sty; | changeset | files |
| Thu, 24 Jan 2002 22:43:40 +0100 | wenzelm | cond_print_result_rule: priority (again) instead of slightly | changeset | files |
| Thu, 24 Jan 2002 22:42:14 +0100 | wenzelm | fixed subgoal_tac; fails on non-existent subgoal; | changeset | files |
| Thu, 24 Jan 2002 22:41:44 +0100 | wenzelm | copy_styles replaces overly conservative update_styles; | changeset | files |
| Thu, 24 Jan 2002 18:22:01 +0100 | wenzelm | Springer LNCS 2283; | changeset | files |
| Thu, 24 Jan 2002 16:37:49 +0100 | wenzelm | updated; | changeset | files |
| Thu, 24 Jan 2002 16:37:43 +0100 | wenzelm | iff del: less_Suc0 -- luckily this does NOT affect the printed text; | changeset | files |
| Wed, 23 Jan 2002 17:13:54 +0100 | wenzelm | delsimps [less_Suc0]; | changeset | files |
| Wed, 23 Jan 2002 17:01:53 +0100 | wenzelm | less_Suc0; | changeset | files |