| Sun, 09 Mar 2014 17:37:34 +0100 |
wenzelm |
more formal read_root;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:08:31 +0100 |
wenzelm |
simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:34:29 +0200 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
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
|
| Sat, 30 Mar 2013 12:13:39 +0100 |
wenzelm |
item markup for Proof_Context.pretty_fact;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 16:16:22 +0100 |
wenzelm |
tuned -- less indirection;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 14:23:33 +0200 |
wenzelm |
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 15:40:41 +0200 |
wenzelm |
separate module Graph_Display;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 11:43:08 +0200 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 22:17:46 +0200 |
wenzelm |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:53:09 +0200 |
wenzelm |
proper binding/report of defined simprocs;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 13:54:07 +0200 |
wenzelm |
added Theory.nodes_of convenience;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +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
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 10:59:43 +0200 |
wenzelm |
renamed Standard_Syntax to Syntax_Phases;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 23:14:41 +0200 |
wenzelm |
moved decode/parse operations to standard_syntax.ML;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 14:25:18 +0200 |
wenzelm |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
file |
diff |
annotate
|
| Sun, 03 Apr 2011 21:59:33 +0200 |
wenzelm |
added Position.reports convenience;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:18 +0100 |
ballarin |
Diagnostic command to show locale dependencies.
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 16:15:31 +0100 |
wenzelm |
added 'syntax_declaration' command;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 15:28:00 +0100 |
wenzelm |
more explicit Isabelle_System operations;
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 19:36:54 +0100 |
wenzelm |
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
|
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
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:31:54 +0200 |
wenzelm |
discontinued obsolete ProofContext.prems_limit;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 21:13:53 +0200 |
wenzelm |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 11:17:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:29:54 +0200 |
wenzelm |
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 18:13:57 +0200 |
wenzelm |
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
print_interps shows interpretations in proofs.
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
file |
diff |
annotate
|
| Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file |
diff |
annotate
|
| Sun, 25 Jul 2010 12:57:29 +0200 |
wenzelm |
Thy_Load.check_loaded via Theory.at_end;
|
file |
diff |
annotate
|
| Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:23:46 +0200 |
wenzelm |
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 13:55:44 +0200 |
wenzelm |
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 22:17:36 +0200 |
wenzelm |
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 21:18:04 +0200 |
wenzelm |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 22:18:59 +0200 |
wenzelm |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 20:17:38 +0200 |
wenzelm |
modernized old-style type abbreviations;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 19:23:03 +0100 |
wenzelm |
added Specification.axiom convenience;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 19:28:25 +0100 |
wenzelm |
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:59:05 +0100 |
wenzelm |
simplified meaning of ProofContext.verbose;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 14:38:36 +0100 |
wenzelm |
print_theorems: suppress concealed (global) facts, unless "!" option is given;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 22:06:46 +0100 |
wenzelm |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 21:05:47 +0100 |
wenzelm |
structure Thm_Deps;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:50:48 +0100 |
wenzelm |
modernized structure Proof_Syntax;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:02:53 +0100 |
wenzelm |
renamed Proof.flat_goal to Proof.simple_goal;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:24:40 +0100 |
wenzelm |
ProofContext.setmp_verbose_CRITICAL;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 22:02:11 +0200 |
wenzelm |
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
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
|
| Sun, 19 Jul 2009 19:24:04 +0200 |
wenzelm |
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
|
file |
diff |
annotate
|
| Sat, 27 Jun 2009 17:35:08 +0200 |
wenzelm |
tune File.isabelle_tool signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 22:43:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 22:38:37 +0200 |
wenzelm |
added Toplevel.previous_node_of;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 22:41:14 +0100 |
wenzelm |
more precise type Symbol_Pos.text;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:43 +0100 |
wenzelm |
ML_Syntax.make_binding;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 23:59:34 +0100 |
wenzelm |
added 'local_setup' command;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 20:31:54 +0100 |
wenzelm |
simplified presentation: pass state directly;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 12:16:12 +0100 |
wenzelm |
proper context for Simplifier.pretty_ss;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 12:07:30 +0100 |
wenzelm |
Theory.add_axioms/add_defs: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:31:41 +0100 |
wenzelm |
oracle: proper name position, tuned;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 19:48:02 +0100 |
wenzelm |
Thm.add_oracle interface: replaced old bstring by binding;
|
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
|
| Sat, 28 Feb 2009 18:00:20 +0100 |
wenzelm |
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 15:46:22 +0100 |
wenzelm |
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 07:53:38 +1100 |
kleing |
New command find_consts searching for constants by type (by Timothy Bourke).
|
file |
diff |
annotate
|
| Wed, 11 Feb 2009 14:48:14 +1100 |
kleing |
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:55:04 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 20:10:22 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 17:32:37 +0100 |
wenzelm |
print_theorems: more robust difference, even after finished proof;
|
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
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
file |
diff |
annotate
|
| Sat, 04 Oct 2008 14:29:43 +0200 |
wenzelm |
renamed isatool to isabelle_tool in programming interfaces;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:38 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 20:13:41 +0200 |
wenzelm |
report doc_source;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 19:52:36 +0200 |
wenzelm |
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
|
file |
diff |
annotate
|