| Sun, 04 Aug 2024 17:39:47 +0200 |
wenzelm |
tuned: more explicit dest_Const_name and dest_Const_type;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 21:03:16 +0100 |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| Thu, 11 May 2023 22:12:43 +0200 |
wenzelm |
proper Thm.trim_context / Thm.transfer;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 20:38:21 +0200 |
wenzelm |
discontinued somewhat pointless antiquotations;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 17:09:05 +0200 |
wenzelm |
tuned antiquotations;
|
file |
diff |
annotate
|
| Tue, 21 Sep 2021 13:14:18 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Sun, 19 Sep 2021 21:55:11 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 19 Sep 2021 21:37:14 +0200 |
wenzelm |
clarified signature -- prefer antiquotations (with subtle change of exception content);
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:28:01 +0200 |
wenzelm |
clarified antiquotation;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:02:12 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 13:04:32 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2019 15:16:53 +0100 |
wenzelm |
clarified contexts;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2019 14:01:06 +0200 |
wenzelm |
more accurate proof definitions (PThm nodes);
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 22:31:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2015 22:16:39 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 15:11:50 +0100 |
wenzelm |
more accurate context;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 22:15:51 +0100 |
wenzelm |
eliminated pointless check -- command definitions are subject to theory context;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2014 18:50:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 12:22:57 +0200 |
wenzelm |
proper context for print_tac;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 15:58:27 +0100 |
wenzelm |
avoid hard-wired theory names;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 17:52:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 14:29:22 +0100 |
wenzelm |
clarified simplifier context;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 17:08:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 17:14:39 +0200 |
wenzelm |
more precise treatment of theory vs. Proof.context;
|
file |
diff |
annotate
|
| Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 18:32:19 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 12:26:48 +0200 |
haftmann |
deglobalization
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
| 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 =)
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:06:29 +0200 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 21:05:54 +0200 |
wenzelm |
more explicit treatment of context, although not fully localized;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 18:07:21 +0100 |
wenzelm |
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 22:30:51 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:39:48 +0100 |
wenzelm |
moved ancient Drule.get_def to OldGoals.get_def;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:38:46 +0100 |
wenzelm |
modernized structure Primitive_Defs;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:48:24 +0200 |
wenzelm |
modernized Balanced_Tree;
|
file |
diff |
annotate
|
| 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.;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 22:05:00 +0100 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:17:25 +0100 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 11:31:40 +0100 |
wenzelm |
MetaSimplifier.SIMPLIFIER;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 23:31:49 +0100 |
wenzelm |
normalized some ML type/val aliases;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 16:07:03 +0200 |
wenzelm |
Thm.get_def;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:10 +0200 |
wenzelm |
eliminated old Sign.read_term/Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:23 +0200 |
wenzelm |
adapted to ProofContext.revert_skolem: extra Name.clean required;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 22:07:26 +0100 |
wenzelm |
proper antiquotations;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2008 14:10:15 +0100 |
wenzelm |
misc cleanup of embedded ML code;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 15:40:21 +0100 |
krauss |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 20:01:37 +0100 |
wenzelm |
avoid redundant escaping of Isabelle symbols;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2007 21:19:31 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 22:00:15 +0200 |
wenzelm |
tuned Induct interface: prefer pred'' over set'';
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2007 22:33:17 +0200 |
wenzelm |
avoid unnamed infixes;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 19:18:01 +0200 |
wenzelm |
Attrib.eval_thms;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|