src/HOL/Tools/inductive_set.ML
Thu, 10 Sep 2015 12:52:24 +0200 haftmann unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sat, 25 Jul 2015 23:41:53 +0200 wenzelm updated to infer_instantiate;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Mon, 01 Jun 2015 13:52:35 +0200 wenzelm obsolete (see 189c81779a68);
Mon, 01 Jun 2015 13:35:16 +0200 wenzelm clarified context;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Tue, 31 Mar 2015 17:34:52 +0200 wenzelm clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
Tue, 31 Mar 2015 00:11:54 +0200 wenzelm tuned signature;
Fri, 06 Mar 2015 23:56:43 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Fri, 08 Aug 2014 20:17:13 +0200 wenzelm observe context visibility -- less redundant warnings;
Thu, 10 Apr 2014 12:48:01 +0200 wenzelm modernized simproc_setup;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
Wed, 01 Jan 2014 14:29:22 +0100 wenzelm clarified simplifier context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 08 Jan 2013 17:10:06 +0100 wenzelm more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";
Wed, 12 Sep 2012 14:46:13 +0200 wenzelm removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
Wed, 05 Sep 2012 19:51:00 +0200 wenzelm discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
Wed, 07 Mar 2012 16:13:49 +0100 berghofe to_pred/set attributes now properly handle variables of type "... => T set"
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Sat, 24 Dec 2011 16:14:58 +0100 haftmann treatment of type constructor `set`
Mon, 07 Nov 2011 14:23:50 +0100 wenzelm clarified attribute "mono_set": pure declaration, proper export in ML;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Wed, 19 Oct 2011 08:37:23 +0200 bulwahn removing old code generator setup for inductive sets in the inductive set package
Mon, 01 Aug 2011 12:08:53 +0200 nipkow infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Mon, 23 Aug 2010 16:47:57 +0200 bulwahn introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
Tue, 20 Jul 2010 23:09:49 +0200 wenzelm discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
Wed, 07 Jul 2010 08:25:21 +0200 bulwahn added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Thu, 10 Jun 2010 12:24:02 +0200 haftmann moved inductive_codegen to place where product type is available; tuned structure name
Wed, 26 May 2010 16:05:25 +0200 haftmann dropped legacy theorem bindings
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Fri, 12 Mar 2010 12:14:31 +0100 bulwahn adding Spec_Rules to definitional package inductive and inductive_set
Mon, 08 Mar 2010 15:00:34 +0100 berghofe Added inducts field to inductive_result.
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Sat, 30 Jan 2010 16:56:28 +0100 berghofe Added "constraints" tag / attribute for specifying the number of equality
Thu, 14 Jan 2010 17:54:55 +0100 haftmann dropped unused binding
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
less more (0) -60 tip