src/HOL/HOL.thy
Sun, 05 Nov 2006 21:44:32 +0100 wenzelm Sign.const_syntax_name;
Fri, 03 Nov 2006 14:22:37 +0100 haftmann simplified reasoning tools setup
Tue, 31 Oct 2006 09:28:55 +0100 haftmann added Equals_conv
Mon, 16 Oct 2006 14:07:31 +0200 haftmann moved HOL code generator setup to Code_Generator
Fri, 13 Oct 2006 12:32:44 +0200 haftmann lifted claset setup from ML to Isar level
Wed, 11 Oct 2006 14:51:24 +0200 haftmann cleaned up HOL bootstrap
Tue, 10 Oct 2006 10:35:24 +0200 haftmann cleanup basic HOL bootstrap
Mon, 02 Oct 2006 23:00:49 +0200 haftmann improved serialization for arbitrary
Thu, 28 Sep 2006 23:42:30 +0200 wenzelm tuned;
Wed, 27 Sep 2006 21:49:34 +0200 wenzelm proper const_syntax for uminus, abs;
Tue, 26 Sep 2006 13:34:16 +0200 haftmann renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
Mon, 25 Sep 2006 17:04:14 +0200 haftmann added 'undefined' serializer
Tue, 19 Sep 2006 15:21:44 +0200 haftmann introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
Fri, 01 Sep 2006 08:36:51 +0200 haftmann final syntax for some Isar code generator keywords
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Thu, 27 Jul 2006 13:43:00 +0200 wenzelm tuned proofs;
Fri, 21 Jul 2006 11:34:01 +0200 berghofe - Added new "undefined" constant
Fri, 07 Jul 2006 09:31:57 +0200 nipkow made evaluation_conv and normalization_conv visible.
Wed, 05 Jul 2006 16:24:28 +0200 paulson removed the "tagging" feature
Fri, 30 Jun 2006 18:26:22 +0200 nipkow normalization uses refl now
Thu, 29 Jun 2006 13:52:28 +0200 nipkow new method "normalization"
Wed, 14 Jun 2006 12:14:42 +0200 haftmann slight adaption for code generator
Tue, 06 Jun 2006 20:42:25 +0200 wenzelm quoted "if";
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Tue, 09 May 2006 14:18:40 +0200 haftmann introduced characters for code generator; some improved code lemmas for some list functions
Tue, 09 May 2006 10:09:17 +0200 haftmann different object logic setup for CodegenTheorems
Tue, 02 May 2006 20:42:32 +0200 wenzelm replaced syntax/translations by abbreviation;
Thu, 06 Apr 2006 16:11:30 +0200 haftmann adapted for definitional code generation
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Thu, 02 Mar 2006 18:49:13 +0100 paulson moved the "use" directive
Wed, 01 Mar 2006 06:08:12 +0100 mengj Added setup for "atpset" (a rule set for ATPs).
Sat, 25 Feb 2006 15:19:47 +0100 haftmann improved codegen bootstrap
Wed, 22 Feb 2006 22:18:32 +0100 wenzelm simplified Pure conjunction;
Tue, 14 Feb 2006 17:07:48 +0100 haftmann added theory of executable rational numbers
Wed, 01 Feb 2006 19:19:32 +0100 berghofe Added "evaluation" method and oracle.
Tue, 31 Jan 2006 16:26:18 +0100 haftmann added serialization for arbitrary
Sun, 29 Jan 2006 19:23:38 +0100 wenzelm declare 'defn' rules;
Mon, 23 Jan 2006 14:07:52 +0100 haftmann removed problematic keyword 'atom'
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Mon, 16 Jan 2006 21:55:14 +0100 wenzelm declare the1_equality [elim?];
Sun, 15 Jan 2006 19:58:51 +0100 wenzelm prefer ex1I over ex_ex1I in single-step reasoning;
Fri, 06 Jan 2006 18:18:13 +0100 wenzelm simplified EqSubst setup;
Fri, 06 Jan 2006 15:18:20 +0100 wenzelm tuned EqSubst setup;
Sat, 31 Dec 2005 21:49:39 +0100 wenzelm removed obsolete cla_dist_concl;
Fri, 30 Dec 2005 16:56:56 +0100 wenzelm provide cla_dist_concl;
Fri, 23 Dec 2005 18:36:26 +0100 wenzelm removed obsolete induct_atomize_old;
Thu, 22 Dec 2005 00:28:36 +0100 wenzelm structure ProjectRule;
Thu, 27 Oct 2005 13:54:38 +0200 wenzelm alternative iff syntax for equality on booleans, with print_mode 'iff';
Sun, 25 Sep 2005 20:19:31 +0200 berghofe eq_codegen now ensures that code for bool type is generated.
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Sat, 17 Sep 2005 18:11:19 +0200 wenzelm added code generator setup (from Main.thy);
Thu, 15 Sep 2005 11:15:52 +0200 paulson the experimental tagging system, and the usual tidying
Tue, 06 Sep 2005 16:59:48 +0200 wenzelm axclass: name space prefix is now "c_class" instead of just "c";
Wed, 31 Aug 2005 15:46:34 +0200 wenzelm simp_implies: proper named infix;
Tue, 02 Aug 2005 16:50:55 +0200 ballarin Turned simp_implies into binary operator.
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
Fri, 01 Jul 2005 13:54:12 +0200 berghofe Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
Tue, 28 Jun 2005 15:27:45 +0200 paulson Constant "If" is now local
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
less more (0) -100 -60 tip