| Tue, 10 Mar 1998 13:23:35 +0100 | nipkow | Removed expand_split from simpset. | changeset | files |
| Mon, 09 Mar 1998 16:30:55 +0100 | wenzelm | removed pred; | changeset | files |
| Mon, 09 Mar 1998 16:17:28 +0100 | wenzelm | eliminated pred function; | changeset | files |
| Mon, 09 Mar 1998 16:16:21 +0100 | wenzelm | Symbol.explode; | changeset | files |
| Mon, 09 Mar 1998 16:15:24 +0100 | wenzelm | replaced $LOGNAME by $USER; | changeset | files |
| Mon, 09 Mar 1998 16:14:46 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 09 Mar 1998 16:14:32 +0100 | wenzelm | Symbol.is_*; | changeset | files |
| Mon, 09 Mar 1998 16:14:15 +0100 | wenzelm | adapted to new scanner, baroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:13:21 +0100 | wenzelm | Symbol.input; | changeset | files |
| Mon, 09 Mar 1998 16:12:39 +0100 | wenzelm | adapted to symbols, scan; | changeset | files |
| Mon, 09 Mar 1998 16:12:19 +0100 | wenzelm | Generic scanners (for potentially infinite input) -- replaces Scanner; | changeset | files |
| Mon, 09 Mar 1998 16:11:50 +0100 | wenzelm | adapted to new scanner and abroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:11:28 +0100 | wenzelm | read_var; | changeset | files |
| Mon, 09 Mar 1998 16:11:13 +0100 | wenzelm | Symbol.output; | changeset | files |
| Mon, 09 Mar 1998 16:10:57 +0100 | wenzelm | tuned syntax error msg; | changeset | files |
| Mon, 09 Mar 1998 16:10:38 +0100 | wenzelm | Symbol.explode; | changeset | files |
| Mon, 09 Mar 1998 16:10:22 +0100 | wenzelm | scan.ML, symbol.ML; | changeset | files |
| Mon, 09 Mar 1998 16:09:56 +0100 | wenzelm | adapted to new scanners and baroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:09:32 +0100 | wenzelm | tuned some names; | changeset | files |
| Mon, 09 Mar 1998 16:09:06 +0100 | wenzelm | adapted to baroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:08:37 +0100 | wenzelm | added merge_alists; | changeset | files |
| Mon, 09 Mar 1998 16:08:06 +0100 | wenzelm | Syntax.indexname; | changeset | files |
| Mon, 09 Mar 1998 16:07:22 +0100 | wenzelm | tuned comment; | changeset | files |
| Mon, 09 Mar 1998 16:07:03 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 09 Mar 1998 16:06:46 +0100 | wenzelm | replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; | changeset | files |
| Mon, 09 Mar 1998 16:05:34 +0100 | wenzelm | replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; | changeset | files |
| Sat, 07 Mar 1998 16:29:29 +0100 | nipkow | Removed `addsplits [expand_if]' | changeset | files |
| Fri, 06 Mar 1998 18:25:28 +0100 | wenzelm | added clasimp.ML; | changeset | files |
| Fri, 06 Mar 1998 16:05:04 +0100 | nipkow | Removed superfluous `op' | changeset | files |
| Fri, 06 Mar 1998 15:58:16 +0100 | nipkow | *** empty log message *** | changeset | files |
| Fri, 06 Mar 1998 15:20:29 +0100 | nipkow | Added delspilts, Addsplits, Delsplits. | changeset | files |
| Fri, 06 Mar 1998 15:19:29 +0100 | nipkow | expand_if is now by default part of the simpset. | changeset | files |
| Thu, 05 Mar 1998 10:47:27 +0100 | paulson | New theorem and simprules | changeset | files |
| Wed, 04 Mar 1998 13:16:05 +0100 | nipkow | Reorganized simplifier. May now reorient rules. | changeset | files |
| Wed, 04 Mar 1998 13:15:05 +0100 | nipkow | Reorganized simplifier. May now reorient rules. | changeset | files |
| Wed, 04 Mar 1998 13:14:11 +0100 | nipkow | Reorganized simplifier. May now reorient rules. | changeset | files |
| Tue, 03 Mar 1998 15:15:04 +0100 | paulson | Better simplification allows deletion of parts of proofs | changeset | files |
| Tue, 03 Mar 1998 15:13:24 +0100 | paulson | New theorem | changeset | files |
| Tue, 03 Mar 1998 15:12:57 +0100 | paulson | New theorems | changeset | files |
| Tue, 03 Mar 1998 15:12:25 +0100 | paulson | New theorems; tidied | changeset | files |
| Tue, 03 Mar 1998 15:11:26 +0100 | paulson | New theorem diff_Suc_le_Suc_diff; tidied another proof | changeset | files |
| Tue, 03 Mar 1998 15:09:04 +0100 | paulson | auto generated | changeset | files |
| Sat, 28 Feb 1998 15:41:50 +0100 | nipkow | Modified def. | changeset | files |
| Sat, 28 Feb 1998 15:41:17 +0100 | nipkow | Splitters via named loopers. | changeset | files |
| Sat, 28 Feb 1998 15:40:50 +0100 | nipkow | Little reorganization. Loop tactics have names now. | changeset | files |
| Sat, 28 Feb 1998 15:40:03 +0100 | nipkow | Tried to reorganize rewriter a little. More to be done. | changeset | files |
| Fri, 27 Feb 1998 11:21:28 +0100 | oheimb | added minimal description of rep_cs: corrections | changeset | files |
| Fri, 27 Feb 1998 11:18:29 +0100 | oheimb | added minimal description of rep_cs | changeset | files |
| Fri, 27 Feb 1998 11:18:16 +0100 | oheimb | added minimal description of rep_ss | changeset | files |
| Fri, 27 Feb 1998 11:08:20 +0100 | paulson | "choice" moved to Set.ML | changeset | files |
| Fri, 27 Feb 1998 11:07:58 +0100 | paulson | New absorbsion laws, etc | changeset | files |
| Fri, 27 Feb 1998 11:07:13 +0100 | paulson | Vimage | changeset | files |
| Fri, 27 Feb 1998 11:06:28 +0100 | paulson | New vimage laws | changeset | files |
| Thu, 26 Feb 1998 15:45:33 +0100 | oheimb | added smart_tac | changeset | files |
| Thu, 26 Feb 1998 15:41:46 +0100 | oheimb | removed superfluous addss | changeset | files |
| Thu, 26 Feb 1998 11:07:57 +0100 | paulson | New theory, Vimage | changeset | files |
| Thu, 26 Feb 1998 11:07:37 +0100 | paulson | Proved choice and bchoice; changed Fun.thy -> thy | changeset | files |
| Thu, 26 Feb 1998 10:48:19 +0100 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 26 Feb 1998 10:41:36 +0100 | wenzelm | added clasimp.ML; | changeset | files |
| Wed, 25 Feb 1998 20:29:58 +0100 | oheimb | renamed rep_claset to rep_cs | changeset | files |