src/HOL/Statespace/state_space.ML
Fri, 21 Aug 2020 18:59:29 +0000 haftmann proper syntax declaration
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 19 Sep 2018 20:45:47 +0200 wenzelm clarified signature;
Tue, 06 Mar 2018 22:59:00 +0100 ballarin Drop rewrite rule arguments of sublocale and interpretation implementations.
Tue, 16 Jan 2018 19:28:05 +0100 ballarin Experimental support for rewrite morphisms in locale instances.
Fri, 04 Aug 2017 08:12:37 +0200 haftmann provide explicit variant initializers for regular named target vs. almost-named target
Wed, 06 Jul 2016 11:29:51 +0200 wenzelm tuned signature;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Sat, 14 Nov 2015 17:37:44 +0100 haftmann represent both algebraic and local-theory views on locale interpretation in interfaces
Sat, 14 Nov 2015 08:45:51 +0100 haftmann separate ML module for interpretation
Mon, 09 Nov 2015 21:04:49 +0100 wenzelm uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Mon, 01 Jun 2015 13:32:36 +0200 wenzelm clarified context;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Wed, 01 Apr 2015 21:12:05 +0200 wenzelm imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;
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.;
Fri, 06 Jun 2014 19:19:46 +0200 haftmann dropped obscure and unused ad-hoc before_exit hook for named targets
Fri, 07 Mar 2014 11:34:41 +0100 wenzelm removed dead code;
Tue, 23 Apr 2013 11:14:50 +0200 haftmann target-sensitive user-level commands interpretation and sublocale
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Mon, 26 Nov 2012 14:43:28 +0100 wenzelm tuned command descriptions;
Wed, 17 Oct 2012 13:20:08 +0200 wenzelm more method position information, notably finished_pos after end of previous text;
Tue, 16 Oct 2012 20:23:00 +0200 wenzelm more proof method text position information;
Wed, 10 Oct 2012 15:21:26 +0200 wenzelm more explicit namespace prefix for 'statespace' -- duplicate facts;
Thu, 09 Aug 2012 12:39:05 +0200 wenzelm tuned 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;
Wed, 14 Mar 2012 20:34:20 +0100 wenzelm locale expressions without source positions;
Fri, 02 Dec 2011 15:23:27 +0100 wenzelm eliminated some legacy operations;
Mon, 28 Nov 2011 17:06:20 +0100 wenzelm tuned messages;
Sun, 06 Nov 2011 17:53:32 +0100 wenzelm misc tuning and modernization;
Sun, 06 Nov 2011 17:05:45 +0100 wenzelm tuned;
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Sat, 16 Apr 2011 20:49:48 +0200 wenzelm proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Wed, 06 Apr 2011 23:04:00 +0200 wenzelm separate structure Term_Position;
Tue, 22 Mar 2011 15:32:47 +0100 wenzelm statespace syntax: strip positions -- type constraints are unexpected here;
Sun, 16 Jan 2011 14:57:14 +0100 wenzelm added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
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, 18 Dec 2010 18:43:13 +0100 ballarin Add mixins to sublocale command.
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 21:22:07 +0200 wenzelm eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
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;
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Thu, 12 Aug 2010 13:28:18 +0200 haftmann Named_Target.init: empty string represents theory target
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target
Thu, 27 May 2010 18:10:37 +0200 wenzelm renamed structure PrintMode to Print_Mode, 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;
less more (0) -100 -60 tip