Fri, 27 Jan 2006 19:03:19 +0100 wenzelm renamed Pretty.gen_list to Pretty.enum;
Fri, 27 Jan 2006 19:03:17 +0100 wenzelm swapped theory_context;
Fri, 27 Jan 2006 19:03:16 +0100 wenzelm swapped Toplevel.theory_context;
Fri, 27 Jan 2006 19:03:15 +0100 wenzelm added invent_fixes;
Fri, 27 Jan 2006 19:03:14 +0100 wenzelm swapped Toplevel.theory_context;
Fri, 27 Jan 2006 19:03:13 +0100 wenzelm renamed reverse_atomize to unatomize;
Fri, 27 Jan 2006 19:03:12 +0100 wenzelm init: include view;
Fri, 27 Jan 2006 19:03:11 +0100 wenzelm improved 'notes', including proper treatment of locale results;
Fri, 27 Jan 2006 19:03:10 +0100 wenzelm swapped Toplevel.theory_context;
Fri, 27 Jan 2006 19:03:09 +0100 wenzelm Locale.init;
Fri, 27 Jan 2006 19:03:08 +0100 wenzelm renamed gen_list to enum;
Fri, 27 Jan 2006 19:03:07 +0100 wenzelm moved theorem tags from Drule to PureThy;
Fri, 27 Jan 2006 19:03:05 +0100 wenzelm added ProofContext.pprint_context (depends on ProofContext.debug);
Fri, 27 Jan 2006 19:03:02 +0100 wenzelm moved theorem tags from Drule to PureThy;
Fri, 27 Jan 2006 18:29:33 +0100 paulson tidying up SPASS output
Fri, 27 Jan 2006 18:29:11 +0100 paulson tidying
Fri, 27 Jan 2006 18:28:55 +0100 paulson better reporting
Fri, 27 Jan 2006 16:05:23 +0100 ballarin Interface to access the specification of a named locale.
Fri, 27 Jan 2006 05:46:39 +0100 mengj Added new file Tools/ATP/reduce_axiomsN.ML
Fri, 27 Jan 2006 05:45:25 +0100 mengj Added in new file Tools/ATP/reduce_axiomsN.ML
Fri, 27 Jan 2006 05:37:12 +0100 mengj Changed codes that call relevance filter.
Fri, 27 Jan 2006 05:34:20 +0100 mengj Relevance filtering. Has replaced the previous version.
Thu, 26 Jan 2006 20:42:15 +0100 webertj interrupt_timeout now raises Interrupt instead of SML90.Interrupt
Thu, 26 Jan 2006 20:17:54 +0100 webertj smaller example to prevent timeout
Thu, 26 Jan 2006 17:58:01 +0100 berghofe Fixed bug in code generator for primitive definitions that
Thu, 26 Jan 2006 15:37:14 +0100 berghofe Inductive sets with no introduction rules are now allowed as well.
Wed, 25 Jan 2006 00:21:44 +0100 wenzelm added definition(_i);
Wed, 25 Jan 2006 00:21:43 +0100 wenzelm renamed export to export_standard (again!), because it includes Drule.local_standard';
Wed, 25 Jan 2006 00:21:42 +0100 wenzelm ProofContext.export_standard;
Wed, 25 Jan 2006 00:21:41 +0100 wenzelm tuned atomize_cterm;
Wed, 25 Jan 2006 00:21:40 +0100 wenzelm turned abstract_term into ProofContext.abs_def;
Wed, 25 Jan 2006 00:21:39 +0100 wenzelm added constant definition;
Wed, 25 Jan 2006 00:21:38 +0100 wenzelm added 'definition';
Wed, 25 Jan 2006 00:21:37 +0100 wenzelm tuned comment;
Wed, 25 Jan 2006 00:21:36 +0100 wenzelm export name_multi;
Wed, 25 Jan 2006 00:21:35 +0100 wenzelm abs_def: improved error;
Wed, 25 Jan 2006 00:21:34 +0100 wenzelm ObjectLogic.atomize_cterm;
Wed, 25 Jan 2006 00:21:32 +0100 wenzelm updated;
Tue, 24 Jan 2006 15:16:06 +0100 webertj works with DPLL solver now
Tue, 24 Jan 2006 13:28:06 +0100 urbanc the additional freshness-condition in the one-induction
Tue, 24 Jan 2006 00:44:39 +0100 wenzelm fixed code_generate syntax;
Tue, 24 Jan 2006 00:43:34 +0100 wenzelm renamed axiomatize(_i) to axiomatization(_i);
Tue, 24 Jan 2006 00:43:33 +0100 wenzelm renamed inferred_type to inferred_param;
Tue, 24 Jan 2006 00:43:32 +0100 wenzelm ProofContext.inferred_param;
Tue, 24 Jan 2006 00:43:31 +0100 wenzelm removed the_params;
Tue, 24 Jan 2006 00:43:29 +0100 wenzelm added actual operations;
Tue, 24 Jan 2006 00:43:28 +0100 wenzelm axiomatization: optional vars;
Tue, 24 Jan 2006 00:43:27 +0100 wenzelm LocalTheory.pretty_consts;
Tue, 24 Jan 2006 00:43:25 +0100 wenzelm tuned;
Tue, 24 Jan 2006 00:43:24 +0100 wenzelm add_finals: prep_consts, i.e. varify type;
Tue, 24 Jan 2006 00:43:23 +0100 wenzelm added dest_all;
Mon, 23 Jan 2006 18:20:48 +0100 webertj TimeLimit replaced by interrupt_timeout
Mon, 23 Jan 2006 17:29:52 +0100 webertj TimeLimit replaced by interrupt_timeout
Mon, 23 Jan 2006 15:23:31 +0100 krauss Updated to Isabelle 2006-01-23
Mon, 23 Jan 2006 15:14:06 +0100 urbanc made change for ex1
Mon, 23 Jan 2006 14:07:52 +0100 haftmann removed problematic keyword 'atom'
Mon, 23 Jan 2006 14:06:40 +0100 haftmann more general serializer
Mon, 23 Jan 2006 14:06:28 +0100 haftmann slight steps forward
Mon, 23 Jan 2006 14:06:11 +0100 haftmann exported after_qed for axclass instance
Mon, 23 Jan 2006 11:41:54 +0100 paulson ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip