src/ZF/Tools/inductive_package.ML
Fri, 27 Apr 2012 22:47:30 +0200 wenzelm clarified signature;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 07 Jan 2011 18:32:19 +0100 wenzelm do not open ML structures;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Wed, 18 Aug 2010 12:26:48 +0200 haftmann deglobalization
Mon, 12 Jul 2010 21:38:37 +0200 wenzelm moved misc legacy stuff from OldGoals to Misc_Legacy;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 16 May 2010 00:02:11 +0200 wenzelm prefer structure Parse_Spec;
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 =)
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Thu, 29 Apr 2010 21:05:54 +0200 wenzelm more explicit treatment of context, although not fully localized;
Sat, 27 Mar 2010 18:07:21 +0100 wenzelm moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
Sun, 28 Feb 2010 22:30:51 +0100 wenzelm more antiquotations;
Fri, 19 Feb 2010 20:39:48 +0100 wenzelm moved ancient Drule.get_def to OldGoals.get_def;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Mon, 02 Nov 2009 20:38:46 +0100 wenzelm modernized structure Primitive_Defs;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Tue, 29 Sep 2009 22:48:24 +0200 wenzelm modernized Balanced_Tree;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Fri, 20 Mar 2009 17:12:37 +0100 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
Thu, 19 Mar 2009 22:05:00 +0100 wenzelm proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Sat, 07 Mar 2009 22:17:25 +0100 wenzelm more uniform handling of binding in packages;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Fri, 02 Jan 2009 11:31:40 +0100 wenzelm MetaSimplifier.SIMPLIFIER;
Thu, 01 Jan 2009 23:31:49 +0100 wenzelm normalized some ML type/val aliases;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 18 Nov 2008 18:25:42 +0100 wenzelm eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
Thu, 23 Oct 2008 16:07:03 +0200 wenzelm Thm.get_def;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Wed, 25 Jun 2008 17:38:34 +0200 wenzelm tuned;
Wed, 18 Jun 2008 18:55:10 +0200 wenzelm eliminated old Sign.read_term/Thm.read_cterm etc.;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Thu, 17 Apr 2008 22:22:23 +0200 wenzelm adapted to ProofContext.revert_skolem: extra Name.clean required;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Sat, 15 Mar 2008 22:07:26 +0100 wenzelm proper antiquotations;
Sat, 01 Mar 2008 14:10:15 +0100 wenzelm misc cleanup of embedded ML code;
Mon, 11 Feb 2008 15:40:21 +0100 krauss Made theory names in ZF disjoint from HOL theory names to allow loading both developments
Sat, 26 Jan 2008 20:01:37 +0100 wenzelm avoid redundant escaping of Isabelle symbols;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Fri, 05 Oct 2007 22:00:15 +0200 wenzelm tuned Induct interface: prefer pred'' over set'';
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
Wed, 03 Oct 2007 22:33:17 +0200 wenzelm avoid unnamed infixes;
Wed, 26 Sep 2007 19:18:01 +0200 wenzelm Attrib.eval_thms;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 14 Aug 2007 13:20:12 +0200 wenzelm PrimitiveDefs.mk_defpair;
Tue, 19 Jun 2007 23:15:38 +0200 wenzelm BalancedTree;
Sat, 14 Apr 2007 17:35:52 +0200 wenzelm cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Tue, 03 Apr 2007 19:24:11 +0200 wenzelm removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Sat, 30 Dec 2006 16:08:00 +0100 wenzelm removed conditional combinator;
Tue, 14 Nov 2006 00:15:38 +0100 wenzelm incorporated IsarThy into IsarCmd;
Sat, 05 Aug 2006 14:52:57 +0200 wenzelm tuned;
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Tue, 10 Jan 2006 19:34:04 +0100 wenzelm generic attributes;
Fri, 16 Dec 2005 09:00:11 +0100 haftmann re-arranged tuples (theory * 'a) to ('a * theory) in Pure
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Wed, 19 Oct 2005 21:52:50 +0200 wenzelm removed add_inductive_x;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
Thu, 08 Sep 2005 16:09:23 +0200 haftmann introduces some modern-style AList operations
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Thu, 14 Jul 2005 19:28:40 +0200 wenzelm no open Logic;
Fri, 17 Jun 2005 18:33:42 +0200 wenzelm Context.names_of;
Wed, 13 Apr 2005 18:45:25 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:12:22 +0100 berghofe Replaced xstring by thmref.
Thu, 12 Dec 2002 11:38:18 +0100 paulson Better treatment of equality in premises of inductive definitions. Less
Fri, 04 Oct 2002 15:23:58 +0200 paulson Fixed bug involving inductive definitions with equalities in the premises.
Wed, 20 Feb 2002 00:53:53 +0100 wenzelm Symbol.bump_string;
Tue, 12 Feb 2002 20:28:27 +0100 wenzelm got rid of explicit marginal comments (now stripped earlier from input);
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 11 Jan 2002 14:53:30 +0100 wenzelm replace gen_all by forall_elim_vars_safe;
Mon, 19 Nov 2001 20:47:57 +0100 wenzelm tuned;
Fri, 16 Nov 2001 22:09:44 +0100 wenzelm actually store "coinduct" rule;
Wed, 14 Nov 2001 23:20:41 +0100 wenzelm case_names;
Wed, 14 Nov 2001 18:46:30 +0100 wenzelm adapted primrec/datatype to Isar;
Tue, 13 Nov 2001 22:20:51 +0100 wenzelm rearranged inductive package for Isar;
Fri, 09 Nov 2001 22:53:41 +0100 wenzelm support co/inductive definitions in new-style theories;
Thu, 04 Oct 2001 15:29:37 +0200 wenzelm qualify MetaSimplifier;
Thu, 13 Jul 2000 23:20:57 +0200 wenzelm adapted PureThy.add_defs_i;
Fri, 05 May 2000 22:37:04 +0200 wenzelm use Sign.simple_read_term;
Mon, 13 Mar 2000 13:28:31 +0100 wenzelm adapted to new PureThy.add_thms etc.;
less more (0) -120 tip