Thu, 19 Jan 2006 21:22:19 +0100 wenzelm Syntax.basic_syn;
Thu, 19 Jan 2006 21:22:18 +0100 wenzelm setup: theory -> theory;
Thu, 19 Jan 2006 21:22:17 +0100 wenzelm tuned setmp;
Thu, 19 Jan 2006 21:22:16 +0100 wenzelm setup: theory -> theory;
Thu, 19 Jan 2006 21:22:15 +0100 wenzelm tuned comments;
Thu, 19 Jan 2006 21:22:14 +0100 wenzelm setup: theory -> theory;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Thu, 19 Jan 2006 15:45:10 +0100 berghofe Use generic Simplifier.simp_add attribute instead
Thu, 19 Jan 2006 14:59:55 +0100 berghofe Re-inserted consts_code declaration accidentally deleted
Thu, 19 Jan 2006 10:22:13 +0100 paulson strengthened some lemmas; simplified some proofs
Wed, 18 Jan 2006 11:55:50 +0100 haftmann substantial improvement in serialization handling
Wed, 18 Jan 2006 02:48:58 +0100 urbanc fixed one proof that broke because of the changes
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Tue, 17 Jan 2006 10:26:50 +0100 paulson these hacks are no longer needed
Tue, 17 Jan 2006 10:26:36 +0100 paulson improved SPASS support
Mon, 16 Jan 2006 21:55:17 +0100 wenzelm case_result: drop_schematic, i.e. be permissive about illegal binds;
Mon, 16 Jan 2006 21:55:15 +0100 wenzelm put_facts: do not pretend local thms were named;
Mon, 16 Jan 2006 21:55:14 +0100 wenzelm declare the1_equality [elim?];
Sun, 15 Jan 2006 20:04:05 +0100 wenzelm tuned;
Sun, 15 Jan 2006 20:00:59 +0100 wenzelm tuned;
Sun, 15 Jan 2006 19:58:57 +0100 wenzelm * Classical: optional weight for attributes;
Sun, 15 Jan 2006 19:58:56 +0100 wenzelm guess: used fixed inferred_type of vars;
Sun, 15 Jan 2006 19:58:55 +0100 wenzelm export add_args;
Sun, 15 Jan 2006 19:58:54 +0100 wenzelm attributes: optional weight;
Sun, 15 Jan 2006 19:58:53 +0100 wenzelm classical attributes: optional weight;
Sun, 15 Jan 2006 19:58:51 +0100 wenzelm prefer ex1I over ex_ex1I in single-step reasoning;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Sat, 14 Jan 2006 17:20:51 +0100 wenzelm tuned;
Sat, 14 Jan 2006 17:15:24 +0100 wenzelm * ML/Isar: simplified treatment of user-level errors;
Sat, 14 Jan 2006 17:14:18 +0100 wenzelm sane ERROR vs. TOPLEVEL_ERROR handling;
Sat, 14 Jan 2006 17:14:17 +0100 wenzelm added Isar.toplevel;
Sat, 14 Jan 2006 17:14:16 +0100 wenzelm Output.error_msg;
Sat, 14 Jan 2006 17:14:15 +0100 wenzelm removed special ERROR handling stuff (transform_error etc.);
Sat, 14 Jan 2006 17:14:14 +0100 wenzelm added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
Sat, 14 Jan 2006 17:14:13 +0100 wenzelm Output.debug;
Sat, 14 Jan 2006 17:14:11 +0100 wenzelm generated code: raise Match instead of ERROR;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Fri, 13 Jan 2006 17:39:41 +0100 paulson blacklist experiments
Fri, 13 Jan 2006 17:39:19 +0100 paulson more readable divide ops
Fri, 13 Jan 2006 17:39:03 +0100 paulson more practical time limit
Fri, 13 Jan 2006 14:43:09 +0100 nipkow *** empty log message ***
Fri, 13 Jan 2006 01:13:17 +0100 wenzelm mixfix: added Structure;
Fri, 13 Jan 2006 01:13:16 +0100 wenzelm uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
Fri, 13 Jan 2006 01:13:15 +0100 wenzelm uniform handling of fixes;
Fri, 13 Jan 2006 01:13:11 +0100 wenzelm uniform handling of fixes;
Fri, 13 Jan 2006 01:13:08 +0100 wenzelm uniform handling of fixes;
Fri, 13 Jan 2006 01:13:06 +0100 wenzelm uniform handling of fixes;
Fri, 13 Jan 2006 01:13:05 +0100 wenzelm tuned;
Fri, 13 Jan 2006 01:13:03 +0100 wenzelm generic_setup: optional argument, defaults to Context.setup();
Fri, 13 Jan 2006 01:13:02 +0100 wenzelm added map_theory, map_proof;
Fri, 13 Jan 2006 01:13:00 +0100 wenzelm removed obsolete sign_of;
Fri, 13 Jan 2006 01:12:59 +0100 wenzelm implicit setup, which admits exception_trace;
Fri, 13 Jan 2006 01:12:58 +0100 wenzelm ProofContext.def_export;
Wed, 11 Jan 2006 18:46:31 +0100 urbanc updated to new induction principle
Wed, 11 Jan 2006 18:39:19 +0100 urbanc cahges to use the new induction-principle (now proved in
Wed, 11 Jan 2006 18:38:32 +0100 urbanc changes to make use of the new induction principle proved by
Wed, 11 Jan 2006 18:21:23 +0100 berghofe Implemented proof of (strong) induction rule.
Wed, 11 Jan 2006 18:20:59 +0100 berghofe Added theorem at_finite_select.
Wed, 11 Jan 2006 17:12:30 +0100 urbanc added lemmas perm_empty, perm_insert to do with
Wed, 11 Jan 2006 17:10:11 +0100 urbanc merged the silly lemmas into the eqvt proof of subtype
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip