| 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 |
| Wed, 23 Jan 2002 16:58:45 +0100 | wenzelm | error "Unexpected end of input"; | changeset | files |
| Wed, 23 Jan 2002 16:58:26 +0100 | wenzelm | reorganized code for predicate text; | changeset | files |
| Wed, 23 Jan 2002 16:58:05 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 23 Jan 2002 16:57:33 +0100 | wenzelm | * HOL: nat_number_of; | changeset | files |
| Wed, 23 Jan 2002 11:43:53 +0100 | paulson | A few more standard simprules, TCs, etc. | changeset | files |
| Tue, 22 Jan 2002 21:19:15 +0100 | wenzelm | qualified_result replaces qualified; | changeset | files |
| Tue, 22 Jan 2002 21:18:36 +0100 | wenzelm | added locale_facts(_i) interface (useful for simple ML proof tools); | changeset | files |
| Mon, 21 Jan 2002 22:27:34 +0100 | wenzelm | full_proofs; | changeset | files |
| Mon, 21 Jan 2002 17:03:38 +0100 | wenzelm | * Pure/show_hyps reset by default (in accordance to existing Isar practice); | changeset | files |
| Mon, 21 Jan 2002 17:02:52 +0100 | wenzelm | reset show_hyps by default (in accordance to existing Isar practice); | changeset | files |
| Mon, 21 Jan 2002 16:28:22 +0100 | wenzelm | save library; | changeset | files |
| Mon, 21 Jan 2002 16:15:16 +0100 | wenzelm | full_atomize; | changeset | files |
| Mon, 21 Jan 2002 15:29:06 +0100 | wenzelm | wild guess at polyml-4.1.2; | changeset | files |
| Mon, 21 Jan 2002 15:28:34 +0100 | wenzelm | options -l and -t; | changeset | files |
| Mon, 21 Jan 2002 14:48:11 +0100 | berghofe | Removed timing function. | changeset | files |
| Mon, 21 Jan 2002 14:47:55 +0100 | paulson | new simprules and classical rules | changeset | files |
| Mon, 21 Jan 2002 14:47:47 +0100 | berghofe | Tuned name mangling function. | changeset | files |
| Mon, 21 Jan 2002 14:45:00 +0100 | berghofe | Made some proofs constructive. | changeset | files |
| Mon, 21 Jan 2002 14:43:38 +0100 | berghofe | datatype_codegen now checks type of constructor. | changeset | files |
| Mon, 21 Jan 2002 13:44:16 +0100 | nipkow | *** empty log message *** | changeset | files |
| Mon, 21 Jan 2002 11:25:45 +0100 | paulson | lexical tidying | changeset | files |
| Mon, 21 Jan 2002 10:52:05 +0100 | paulson | slight re-use of code | changeset | files |
| Sat, 19 Jan 2002 15:44:53 +0100 | kleing | fixed typos | changeset | files |
| Fri, 18 Jan 2002 18:36:19 +0100 | wenzelm | rewrite_term: removed rew0, so no on-the-fly eta-contraction; | changeset | files |
| Fri, 18 Jan 2002 18:35:39 +0100 | wenzelm | fixed document setup of HOL-Library; | changeset | files |
| Fri, 18 Jan 2002 18:30:19 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 18 Jan 2002 17:46:17 +0100 | paulson | tidied | changeset | files |
| Fri, 18 Jan 2002 17:45:19 +0100 | paulson | OOPS | changeset | files |
| Fri, 18 Jan 2002 17:44:15 +0100 | paulson | tweaks | changeset | files |
| Fri, 18 Jan 2002 15:17:47 +0100 | wenzelm | moved document sources to proper place, *within* Library/Library (!); | changeset | files |
| Thu, 17 Jan 2002 21:07:11 +0100 | wenzelm | cover polyml-4.1.2; | changeset | files |