Sat, 18 Mar 2006 09:58:49 +0100 haftmann renamed constant less in lattice
Fri, 17 Mar 2006 22:33:06 +0100 nipkow fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
Fri, 17 Mar 2006 17:38:38 +0100 schirmer added parser locale_expr_unless
Fri, 17 Mar 2006 16:17:38 +0100 haftmann fixed clsvar bug
Fri, 17 Mar 2006 15:22:40 +0100 ballarin add_locale(_i) returns internal locale name.
Fri, 17 Mar 2006 14:20:24 +0100 haftmann added example for operational classes and code generator
Fri, 17 Mar 2006 14:19:24 +0100 haftmann slight improvement in serializer, stub for code generator theorems added
Fri, 17 Mar 2006 10:04:27 +0100 ballarin Renamed setsum_mult to setsum_right_distrib.
Fri, 17 Mar 2006 09:57:25 +0100 ballarin Internal restructuring: local parameters.
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Thu, 16 Mar 2006 20:19:25 +0100 ballarin New interface function parameters_of_expr.
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.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip