Wed, 15 Mar 2006 17:59:33 +0100 berghofe add_inst_arity_i renamed to prove_arity.
Wed, 15 Mar 2006 16:18:12 +0100 wenzelm rename_frees: treat trivial names;
Tue, 14 Mar 2006 22:07:33 +0100 wenzelm added singleton;
Tue, 14 Mar 2006 22:06:43 +0100 wenzelm updated;
Tue, 14 Mar 2006 22:06:42 +0100 wenzelm turned string_of_mixfix into pretty_mixfix;
Tue, 14 Mar 2006 22:06:40 +0100 wenzelm added monomorphic;
Tue, 14 Mar 2006 22:06:39 +0100 wenzelm added 'print_statement' command;
Tue, 14 Mar 2006 22:06:37 +0100 wenzelm added print_stmts;
Tue, 14 Mar 2006 22:06:36 +0100 wenzelm added pretty_statement;
Tue, 14 Mar 2006 22:06:35 +0100 wenzelm added command, keyword;
Tue, 14 Mar 2006 22:06:33 +0100 wenzelm Output.add_mode: keyword component;
Tue, 14 Mar 2006 22:06:31 +0100 wenzelm string_of_mixfix;
Tue, 14 Mar 2006 22:06:29 +0100 wenzelm print_statement;
Tue, 14 Mar 2006 16:29:39 +0100 wenzelm added remove_trrules(_i);
Tue, 14 Mar 2006 16:29:38 +0100 wenzelm added is_elim (from Provers/classical.ML);
Tue, 14 Mar 2006 16:29:37 +0100 wenzelm added 'no_translations';
Tue, 14 Mar 2006 16:29:36 +0100 wenzelm added pretty_stmt;
Tue, 14 Mar 2006 16:29:35 +0100 wenzelm declared_const: check for type constraint only, i.e. admit abbreviations as well;
Tue, 14 Mar 2006 16:29:34 +0100 wenzelm ObjectLogic.is_elim;
Tue, 14 Mar 2006 16:29:32 +0100 wenzelm tuned constdecl;
Tue, 14 Mar 2006 16:29:31 +0100 wenzelm updated;
Tue, 14 Mar 2006 16:29:29 +0100 wenzelm Pure: no_translations;
Tue, 14 Mar 2006 14:25:09 +0100 haftmann refined representation of instance dictionaries
Mon, 13 Mar 2006 10:41:04 +0100 schirmer entry for Library/AssocList
Mon, 13 Mar 2006 00:09:23 +0100 berghofe First version of function for defining graph of iteration combinator.
Sat, 11 Mar 2006 21:23:10 +0100 wenzelm got rid of type Sign.sg;
Sat, 11 Mar 2006 17:30:35 +0100 wenzelm renamed plus to add;
Sat, 11 Mar 2006 17:24:37 +0100 wenzelm renamed const minus to subtract;
Sat, 11 Mar 2006 16:56:09 +0100 wenzelm simplified AxClass interfaces;
Sat, 11 Mar 2006 16:53:28 +0100 wenzelm added axclass_instance_XXX (from axclass.ML);
Sat, 11 Mar 2006 16:53:27 +0100 wenzelm *** empty log message ***
Sat, 11 Mar 2006 16:53:23 +0100 wenzelm added read_class, read/cert_classrel/arity (from axclass.ML);
Sat, 11 Mar 2006 16:53:20 +0100 wenzelm moved read_class, read/cert_classrel/arity to sign.ML;
Sat, 11 Mar 2006 16:53:14 +0100 wenzelm use axclass.ML earlier (in Isar/ROOT.ML);
Sat, 11 Mar 2006 16:53:10 +0100 wenzelm nbe: no_document;
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
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip