tuned signature;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

prefer control symbol antiquotations;

tuned;

suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';

more symbols;

tuned signature: more uniform Keyword.spec;

find dynamic facts as well, but static ones are preferred;
tuned;

eliminated "xname" and variants;

clarified bootstrap -- more uniform use of ML files;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

moved remaining display.ML to more_thm.ML;

clarified markup;
tuned signature;

trim context for persistent storage;

improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);

proper context for Object_Logic operations;

@{command_spec} is superseded by @{command_keyword};

more position information and PIDE markup for command keywords;

tuned;

tuned signature;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

eta-expand all search patterns using schematic place holders

--HG--
extra : rebase_source : 4e479e077c25f8f031fc3baaeced85a1ccb26afa

revert "better" handling of abbreviation from c61fe520602b

--HG--
extra : rebase_source : 42ccc22d6c60ba23b560fc3765bb1e76b7af5ad5

tuned variable names

--HG--
extra : rebase_source : 1a6de9230a570260f22783855b931ab7a6699b9b

turn application-specific Pattern.matches_subterm into an application-private function

--HG--
extra : rebase_source : d589025f6bea2a7c23483cf2e57830856d9fafb2

tuned signature;

renamed "pairself" to "apply2", in accordance to @{apply 2};

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

tuned signature;

more frugal keywords;

explicit type Keyword.keywords;
tuned signature;

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

eliminated aliases;

tuned signature according to Scala version -- prefer explicit argument;

tuned comment;

tuned message;

some position markup to help locating the query context, e.g. from "Info" dockable;

tuned message: more compact, imitate actual command line;

tuned message -- more context for detached window etc.;

removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;

tuned option name;

more uniform ML/document antiquotations;

clarified local facts;

more explicit treatment of verbose mode, which includes concealed entries;

more accurate resolution of hybrid facts, which actually changes the sort order of results;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
more thorough background_notes: distribute global notes to all contexts;

more direct Long_Name.qualification;

support for completion within the formal context;
tuned signature;

removed remains of old experiment (see b933142e02d0);

removed dead code;
more complete patterns;

tuned signature;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

print find_thms result in reverse order so best result is on top

more useful sorting of find_thms results

clarified Query_Operation.register: avoid hard-wired parallel policy;
sledgehammer: more conventional parallel exception handling -- print just one interrupt;

prefer local facts over global ones

--HG--
extra : rebase_source : 87d5d7583f9ab9e35bdfa98f181e5fc9a35b76b7

use local context for name space

--HG--
extra : rebase_source : 06d2e4701a53dcf5440b1b08723c4e10bd9be6f8

enable search in pre-loaded theory;

more GUI options;

tuned signature;

tuned;

more explicit error;

tuned message;

removed unused YXML_Find_Theorems and Legacy_XML_Syntax;

more robust read_query;
avoid pointless position, which is always line 1 for single-line input;

slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;

more message markup, provided by prover;

some actual find_theorems functionality;

more general Output.result: allow to update arbitrary properties;
clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);

minimal print function "find_theorems", which merely echos its arguments;

type theory is purely value-oriented;

modify background theory where it is actually required (cf. 51dfdcd88e84);

tuned messages -- avoid text folds stemming from Pretty.chunks;

proper system options for 'find_theorems';

guard unify tracing via visible status of global theory;
find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;

simplifier uses proper Proof.context instead of historic type simpset;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;

--HG--
rename : src/Pure/Tools/xml_syntax.ML => src/Pure/Tools/legacy_xml_syntax.ML

tuned command descriptions;

more formal markup;

more official command specifications, including source position;

slightly more parallel find_theorems;

outer syntax command definitions based on formal command_spec derived from theory header declarations;

tuned;

removed broken/unused introiff (cf. d452117ba564);

discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);

prefer uniform Timing.message -- avoid assumption about sequential execution;

tuned XML modules;

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;

simplified XML_Data;

tuned layout;

parameterize print_theorems over actual search function

(de)serialization for search query and result

explicit type for search queries

moved questionable goal modification out of filter_theorems

exported raw query parser; removed inconsistent clone

separate query parsing from actual search

more conventional naming scheme: names_long, names_short, names_unique;

modernized structure Proof_Context;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;

reactivate time measurement (partly reverting c27b0b37041a);
export pretty_theorem, to display both internal or external facts

generalize find_theorems filters to work on raw propositions, too

Refactor find_theorems to provide a more general filter_facts method

fix non-exhaustive pattern match in find_theorems

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

misc tuning and simplification;

simplified/unified command setup;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;

modernized structure Object_Logic;

modernized structure Term_Ord;

avoid negative indices as argument ot drop

Expand nested abbreviations before applying dummy patterns.

Expand nested abbreviations before applying dummy patterns.

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

observe usual naming conventions;

find_theorems: respect conceal flag

less hermetic ML;
parse_pattern: apply Consts.intern only once (Why is this done anyway?);
modernized structure names;

renamed Proof.flat_goal to Proof.simple_goal;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

dropped redundant gen_ prefix

find_theorems: better handling of abbreviations (by Timothy Bourke)

uniform use of Integer.min/max;

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;

misc tuning and simplification;
be explicit about expressions involving infixes with non-obvious priorities;
removed dead code;
some attempts to recover basic Isabelle coding conventions;

explicit indication of Unsynchronized.ref;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

more detailed start_timing/end_timing;

minor tuning according to Isabelle/ML conventions;
slightly less combinators;

Prototype introiff option for find_theorems.

This feature was suggested by Jeremy Avigad / Tobias Nipkow.

It adds an introiff keyword for find_theorems that returns, in
addition to the usual results for intro, any theorems of the
form ([| ... |] ==> (P = Q)) where either P or Q matches the
conclusions of the current goal. Such theorems can be made
introduction rules with [THEN iffDx].

The current patch is for evaluation only. It assumes an
(op = : 'a -> 'a -> bool) operator, which is specific to HOL.
It is not clear how this should be generalised.

superficial tuning;

Limit the number of results returned by auto_solves.

Use assms rather than prems in find_theorems solves.

Assumption.all_prems_of, Assumption.all_assms_of;

moved basic algebra of long names from structure NameSpace to Long_Name;

replaced archaic use of rep_ss by Simplifier.mksimps;

renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);

nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;

avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
minor tuning according to Isabelle coding conventions;

observe basic Isabelle/ML coding conventions;

moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;

--HG--
rename : src/Pure/Isar/find_consts.ML => src/Pure/Tools/find_consts.ML
rename : src/Pure/Isar/find_theorems.ML => src/Pure/Tools/find_theorems.ML