Fri, 10 Mar 2006 19:49:58 +0100 wenzelm tuned;
Fri, 10 Mar 2006 17:57:09 +0100 paulson exporting reapAll and killChild
Fri, 10 Mar 2006 17:53:53 +0100 webertj text delimiter fixed
Fri, 10 Mar 2006 17:24:16 +0100 webertj comment delimiter fixed
Fri, 10 Mar 2006 16:31:50 +0100 webertj clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
Fri, 10 Mar 2006 16:21:49 +0100 haftmann fix for document preparation
Fri, 10 Mar 2006 16:05:34 +0100 schirmer Added Library/AssocList.thy
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Fri, 10 Mar 2006 12:28:38 +0100 paulson Changed some warnings to debug messages
Fri, 10 Mar 2006 12:27:36 +0100 paulson Frequency analysis of constants (with types).
Fri, 10 Mar 2006 04:03:48 +0100 mengj Shortened the exception messages from assume.
Fri, 10 Mar 2006 04:02:53 +0100 mengj METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
Fri, 10 Mar 2006 00:53:28 +0100 huffman added many simple lemmas
Thu, 09 Mar 2006 06:05:01 +0100 mengj Added more functions to the signature and tidied up some functions.
Wed, 08 Mar 2006 21:40:46 +0100 wenzelm tuned;
Wed, 08 Mar 2006 18:52:43 +0100 urbanc tuned some proofs
Wed, 08 Mar 2006 18:37:31 +0100 wenzelm select_goals: split original conjunctions;
Wed, 08 Mar 2006 18:37:30 +0100 wenzelm method: goal restriction defaults to [1];
Wed, 08 Mar 2006 18:37:28 +0100 wenzelm infer_derivs: avoid allocating empty MinProof;
Wed, 08 Mar 2006 18:37:27 +0100 wenzelm tuned;
Wed, 08 Mar 2006 18:37:25 +0100 wenzelm Isar/method: goal restriction;
Wed, 08 Mar 2006 18:37:24 +0100 wenzelm constdecl: always allow 'where';
Wed, 08 Mar 2006 18:00:00 +0100 urbanc deleted some proofs "on comment"
Wed, 08 Mar 2006 17:55:51 +0100 urbanc tuned some proofs
Wed, 08 Mar 2006 17:54:55 +0100 urbanc tuned some of the proofs about fresh_fun
Wed, 08 Mar 2006 17:23:46 +0100 haftmann first running version of type classes
Wed, 08 Mar 2006 17:03:19 +0100 haftmann first running version of type classes
Wed, 08 Mar 2006 16:29:07 +0100 haftmann first running version of type classes
Wed, 08 Mar 2006 10:19:57 +0100 paulson Frequency strategy. Revised indentation, etc.
Wed, 08 Mar 2006 10:06:31 +0100 nipkow *** empty log message ***
Tue, 07 Mar 2006 18:02:11 +0100 obua added ROOT.ML
Tue, 07 Mar 2006 16:50:33 +0100 paulson Indentation
Tue, 07 Mar 2006 16:49:48 +0100 paulson Tidying and restructuring.
Tue, 07 Mar 2006 16:49:12 +0100 paulson Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
Tue, 07 Mar 2006 16:47:51 +0100 paulson Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
Tue, 07 Mar 2006 16:46:54 +0100 paulson Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
Tue, 07 Mar 2006 16:45:04 +0100 paulson Tidying, and getting rid of SELECT_GOAL (as it does something different now)
Tue, 07 Mar 2006 16:03:31 +0100 obua Added HOL-ZF to Isabelle.
Tue, 07 Mar 2006 14:09:48 +0100 haftmann substantial improvement in codegen iml
Tue, 07 Mar 2006 04:06:02 +0100 mengj Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
Tue, 07 Mar 2006 04:04:21 +0100 mengj relevance_filter takes input axioms as Term.term.
Tue, 07 Mar 2006 04:01:25 +0100 mengj Proof reconstruction now only takes names of theorems as input.
Tue, 07 Mar 2006 03:59:48 +0100 mengj Added tptp_write_file to write all necessary ATP input clauses to one file.
Tue, 07 Mar 2006 03:58:50 +0100 mengj tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
Tue, 07 Mar 2006 03:56:59 +0100 mengj Added functions to retrieve local and global atpset rules.
Tue, 07 Mar 2006 03:54:11 +0100 mengj Moved the settings for ATP time limit to res_atp.ML
Tue, 07 Mar 2006 03:51:40 +0100 mengj Merged res_atp_setup.ML into res_atp.ML.
Tue, 07 Mar 2006 03:49:26 +0100 mengj When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
Tue, 07 Mar 2006 03:48:02 +0100 mengj Merged res_atp_setup.ML into res_atp.ML.
Sun, 05 Mar 2006 23:56:57 +0100 wenzelm SELECT_GOAL: fixed trivial case;
Sun, 05 Mar 2006 18:49:13 +0100 webertj fixed a typo in a comment
Sat, 04 Mar 2006 21:39:08 +0100 wenzelm tuned;
Sat, 04 Mar 2006 21:10:12 +0100 wenzelm method: SelectGoals;
Sat, 04 Mar 2006 21:10:11 +0100 wenzelm method: syntax for SelectGoals;
Sat, 04 Mar 2006 21:10:10 +0100 wenzelm text: added SelectGoals;
Sat, 04 Mar 2006 21:10:09 +0100 wenzelm tuned conj_curry;
Sat, 04 Mar 2006 21:10:08 +0100 wenzelm added extract, retrofit;
Sat, 04 Mar 2006 21:10:07 +0100 wenzelm added mk_conjunction;
Sat, 04 Mar 2006 21:10:06 +0100 wenzelm method: restriction to first n sub-goals;
Fri, 03 Mar 2006 19:43:46 +0100 nipkow minor changes
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip