src/HOL/Tools/inductive_set_package.ML
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
Fri, 14 Nov 2008 08:50:09 +0100 haftmann Name.is_nothing
Fri, 07 Nov 2008 08:57:15 +0100 haftmann exported codegen_preproc
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Sat, 24 May 2008 22:04:52 +0200 wenzelm more uniform treatment of OuterSyntax.local_theory commands;
Wed, 07 May 2008 10:57:19 +0200 berghofe Adapted to encoding of sets as predicates
Thu, 03 Apr 2008 17:54:19 +0200 berghofe Added skip_mono flag and inductive_flags type.
Sat, 29 Mar 2008 13:03:05 +0100 wenzelm eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Mon, 25 Feb 2008 16:31:15 +0100 wenzelm inductive package: simplified group handling;
Thu, 07 Feb 2008 14:39:19 +0100 berghofe Instead of raising an exception, pred_set_conv now ignores conversion
Sat, 26 Jan 2008 17:08:36 +0100 wenzelm added theorem group;
Wed, 28 Nov 2007 14:56:38 +0100 berghofe to_set now applies collect_mem_simproc as well.
Tue, 13 Nov 2007 10:50:33 +0100 berghofe to_pred and to_set now save induction and case rule tags.
Sat, 13 Oct 2007 17:16:39 +0200 wenzelm renamed LocalTheory.def to LocalTheory.define;
Tue, 09 Oct 2007 17:10:32 +0200 wenzelm removed LocalTheory.defs, use plain LocalTheory.def;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Tue, 02 Oct 2007 22:23:26 +0200 wenzelm tuned internal interfaces: flags record, added kind for results;
Fri, 28 Sep 2007 10:30:51 +0200 berghofe add_inductive_i now takes typ instead of typ option as argument.
Fri, 10 Aug 2007 17:04:34 +0200 haftmann new structure for code generator modules
Sun, 29 Jul 2007 14:29:54 +0200 wenzelm renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
Thu, 19 Jul 2007 15:37:37 +0200 berghofe strong_ind_simproc now only rewrites arguments of inductive predicates.
Wed, 11 Jul 2007 11:43:31 +0200 berghofe New wrapper for defining inductive sets with new inductive
less more (0) tip