some export of foundational theory content;

tuned signature;
clarified modules;

more accessible src/Pure/ROOT.ML;

clarified modules: uniform notion of formal comments;

clarified modules;

check bibtex database on ML side -- for semantic PIDE editing;
tuned signature;

clarified directories;

--HG--
rename : src/Pure/Tools/bibtex.ML => src/Pure/Thy/bibtex.ML
rename : src/Pure/Tools/bibtex.scala => src/Pure/Thy/bibtex.scala

PIDE markup for session ROOT files;

clarified file name;

--HG--
rename : src/Pure/ML/ml_pervasive.ML => src/Pure/ML/ml_init.ML

system option for default command tags;

exclude theories from other sessions;
clarified modules;

clarified modules;

more tight implementation of symbol explode operation (without support for raw symbols);

clarified modules;

--HG--
rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML

clarified bootstrap;

ML pp for Rat.rat;

rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;

--HG--
rename : src/Tools/rat.ML => src/Pure/General/rat.ML

common entity definitions within a global or local theory context;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

clarified files;

--HG--
rename : src/Pure/ML/ml_pervasive0.ML => src/Pure/ML/ml_pervasive.ML

clarified modules;
removed unsed exn_id;

shared output primitives of physical/virtual Pure;

clarified bootstrap;

clarified modules;

section headings for ROOT.ML;

back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;

clarified mode of ROOT.ML files;

more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

clarified editor mode;

virtual thread data via context, for proper support of Context.>> etc;

clarified bootstrap;

clarified modules;
tuned signature;

clarified ML bootstrap;

--HG--
rename : src/Pure/ML/ml_pervasive_initial.ML => src/Pure/ML/ml_pervasive0.ML
rename : src/Pure/ML/ml_pervasive_final.ML => src/Pure/ML/ml_pervasive1.ML

clarified files;

--HG--
rename : src/Pure/ML/ML_Root.thy => src/Pure/ML_Root.thy

back to static conditional compilation -- simplified bootstrap;

clarified modules -- simplified bootstrap;

actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;

prefer antiquotations;

proper use_thy;

more uniform ML file commands;

clarified bootstrap -- avoid conditional compilation in ROOT.ML;

tuned;

clarified modules;

--HG--
rename : src/Pure/ML/ml_final.ML => src/Pure/ML/ml_pervasive_final.ML
rename : src/Pure/ML/ml_pervasive.ML => src/Pure/ML/ml_pervasive_initial.ML

clarified conditional compilation;

clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;

clarified bootstrap -- more uniform use of ML files;

clarified bootstrap;

clarified final setup of ML environment;

clarified modules;

structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;

clarified modules;

clarified modules;

explicit print_depth for the sake of Spec_Check.determine_type;

eliminated duplicate;

discontinued slightly odd "secure" mode;

clarified modules;

clarified modules;

--HG--
rename : src/Pure/ML/install_pp_polyml.ML => src/Pure/ML/ml_pp.ML

@{make_string} is available during Pure bootstrap;

clarified modules;

hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;

obsolete;

tuned signature;

eliminated without magic name;

clarified files;

--HG--
rename : src/Pure/Concurrent/random.ML => src/Pure/General/random.ML

clarified files;

--HG--
rename : src/Pure/Concurrent/bash.ML => src/Pure/System/bash.ML
rename : src/Pure/Concurrent/bash.scala => src/Pure/System/bash.scala
rename : src/Pure/Concurrent/bash_windows.ML => src/Pure/System/bash_windows.ML

isabelle.Build uses ML_Process directly;
isabelle_process is for batch mode only;
removed unused feeder (already part of "isabelle console");

discontinued cd, pwd;

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

tuned signature -- clarified modules;

discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;

--HG--
rename : src/Pure/RAW/multithreading.ML => src/Pure/Concurrent/multithreading.ML
rename : src/Pure/RAW/unsynchronized.ML => src/Pure/Concurrent/unsynchronized.ML
rename : src/Pure/RAW/exn.ML => src/Pure/General/exn.ML
rename : src/Pure/RAW/exn.scala => src/Pure/General/exn.scala
rename : src/Pure/RAW/secure.ML => src/Pure/General/secure.ML
rename : src/Pure/RAW/fixed_int_dummy.ML => src/Pure/ML/fixed_int_dummy.ML
rename : src/Pure/RAW/ml_compiler0.ML => src/Pure/ML/ml_compiler0.ML
rename : src/Pure/RAW/ml_debugger.ML => src/Pure/ML/ml_debugger.ML
rename : src/Pure/RAW/ml_heap.ML => src/Pure/ML/ml_heap.ML
rename : src/Pure/RAW/ml_name_space.ML => src/Pure/ML/ml_name_space.ML
rename : src/Pure/RAW/ml_pretty.ML => src/Pure/ML/ml_pretty.ML
rename : src/Pure/RAW/ml_profiling.ML => src/Pure/ML/ml_profiling.ML
rename : src/Pure/RAW/ml_system.ML => src/Pure/ML/ml_system.ML

discontinued polyml-5.3.0;

--HG--
rename : src/Pure/RAW/ml_debugger_polyml-5.6.ML => src/Pure/RAW/ml_debugger.ML
rename : src/Pure/RAW/ml_name_space_polyml-5.6.ML => src/Pure/RAW/ml_name_space.ML
rename : src/Pure/RAW/ml_profiling_polyml-5.6.ML => src/Pure/RAW/ml_profiling.ML

support for ML_exception_debugger;

clarified modules;

--HG--
rename : src/Pure/RAW/compiler_polyml.ML => src/Pure/RAW/ml_compiler0.ML

load secure.ML earlier;
eliminated obsolete ml_parse.ML;
tuned signature;

--HG--
rename : src/Pure/General/secure.ML => src/Pure/RAW/secure.ML

ML debugger support in Pure (again, see 3565c9f407ec);

support only polyml-5.3.0 and polyml-5.6;

--HG--
rename : lib/scripts/run-polyml-5.6 => lib/scripts/run-polyml
rename : lib/scripts/run-polyml => lib/scripts/run-polyml-5.3.0
rename : src/Pure/ML/ml_statistics_polyml-5.5.0.ML => src/Pure/ML/ml_statistics.ML
rename : src/Pure/RAW/exn_trace_polyml-5.5.1.ML => src/Pure/RAW/exn_trace.ML

unconditional Multithreading;
clarified files;

tuned;

clarified file names;

--HG--
rename : src/Pure/ML/exn_output_polyml.ML => src/Pure/ML/exn_output.ML
rename : src/Pure/ML/exn_properties_polyml.ML => src/Pure/ML/exn_properties.ML
rename : src/Pure/ML/ml_compiler_polyml.ML => src/Pure/ML/ml_compiler.ML

SML/NJ is no longer supported;

discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;

--HG--
rename : src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML
rename : src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML
rename : src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
rename : src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_stack_polyml-5.6.ML

speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;

--HG--
rename : lib/scripts/run-polyml-5.5.3 => lib/scripts/run-polyml-5.6

separate ML module for interpretation

--HG--
extra : rebase_source : 867de135491ddc9e949d932384cce64f60343123

clarified modules;

clarified modules;

--HG--
rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML
rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala

load markdown.ML into Pure;

moved remaining display.ML to more_thm.ML;

more explicit Defs.context: use proper name spaces as far as possible;

basic setup for native Windows (RAW session without image);

no ML_debugger support in Pure -- too complicated;

more careful propagation of ML_debugger option to Pure;

support for ML files with/without debugger information;

explicit debug flag for ML compiler;

clarified context;

default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;

clarified module;

--HG--
rename : src/Pure/subgoal.ML => src/Pure/Isar/subgoal.ML

added command 'experiment';

tuned protocol -- resolve command positions in ML;

tuned bootstrap;

--HG--
rename : src/Pure/ML/exn_trace_polyml-5.5.1.ML => src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML

added Path.decode in ML, in correspondence to Path.encode in Scala;

explicit message channel for "legacy", which is nonetheless a variant of "warning";

more toplevel pretty printing;

separate module Random;
proper Synchronized.var;

node-specific keywords, with session base syntax as default;

more abstract type Input.source;

load simple_thread.ML later, such that it benefits from redefined print_exception_trace;

removed some add-ons from modules that are relevant for the inference kernel;

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;

explicit type Keyword.keywords;
tuned signature;

discontinued Isar TTY loop;

discontinued Proof General;

obsolete;

clarified load order;
tuned signature;

pro-forma support for polyml-5.5.3 (presently SVN 1960);

--HG--
rename : lib/scripts/run-polyml-5.5.2 => lib/scripts/run-polyml-5.5.3
rename : src/Pure/ML-Systems/polyml-5.5.2.ML => src/Pure/ML-Systems/polyml-5.5.3.ML

clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

clarified modules;

tuned signature -- prefer self-contained user-space tool;

--HG--
rename : src/Pure/Thy/thm_deps.ML => src/Pure/Tools/thm_deps.ML

load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;

separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;

further distinction of Isabelle distribution: alert for identified release candidates;

more source positions;

clarified ML bootstrap;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

tuned comments;

tuned load order;

proper configuration option "ML_print_depth";
proper ML_exception_trace for HOL-TPTP;

tuned error, according to "use" in General/secure.ML;

clarified module arrangement;

--HG--
rename : src/Pure/System/session.ML => src/Pure/PIDE/session.ML
rename : src/Pure/System/session.scala => src/Pure/PIDE/session.scala

clarifed module name;

--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala

clarified module arrangement;
more antiquotations;

clarified modules;
more antiquotations for antiquotations;

clarified bootstrap process: switch to ML with context and antiquotations earlier;

tuned signature -- clarified module name;

--HG--
rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML

tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;

support for completion within the formal context;
tuned signature;

prefer user-space tool within Pure.thy;

seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;

prefer self-contained user-space tool;

prefer user-space tool within Pure.thy;

--HG--
rename : src/Pure/Thy/rail.ML => src/Pure/Tools/rail.ML

maintain morphism names for diagnostic purposes;

support for polml-5.5.2;
support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890);
clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;

--HG--
rename : lib/scripts/run-polyml-5.5.1 => lib/scripts/run-polyml-5.5.2

toplevel function "use" refers to raw ML bootstrap environment;

updated to polyml-5.5.1;

improved printing of exception trace in Poly/ML 5.5.1;

moved module into plain Isabelle/ML user space;

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

added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;

maintain goal forks as part of global execution;
tuned;

removed unused YXML_Find_Theorems and Legacy_XML_Syntax;

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

exception trace for Poly/ML 5.5.1, using regular Isabelle output;

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

type theory is purely value-oriented;

clarified module name;

--HG--
rename : src/Pure/PIDE/exec.ML => src/Pure/PIDE/execution.ML

global management of command execution fragments;
tuned;

more abstract message channel;

more uniform Counter in ML and Scala;

tuned signature;
tuned comments;

explicit module Document_ID as source of globally unique identifiers across ML/Scala;

tuned signature;

backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;

manage option "proofs" within theory context -- with minor overhead for primitive inferences;

explicit support for type annotations within printed syntax trees;
eliminated obsolete show_free_types;

tuned structure

proper option quick_and_dirty;

event timer as separate service thread;

moved files;

--HG--
rename : src/Pure/ProofGeneral/proof_general.ML => src/Pure/Tools/proof_general.ML
rename : src/Pure/ProofGeneral/proof_general_pure.ML => src/Pure/Tools/proof_general_pure.ML

maintain ProofGeneral preferences within ProofGeneral module;
initialize Isabelle/Pure preferences within normal user space (with antiquotations);
tuned;

just one ProofGeneral module;

--HG--
rename : src/Pure/ProofGeneral/proof_general_emacs.ML => src/Pure/ProofGeneral/proof_general.ML

simplified modules and exceptions;

more direct output of remaining PGIP rudiments;

removed obsolete PGIP material;

support for system options as context-sensitive config options;

removed redundant modules;

additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

tuned signature and module arrangement;

--HG--
rename : src/Pure/Isar/skip_proof.ML => src/Pure/skip_proof.ML

tuned order of modules;

more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;

recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;

slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);

moved files;

--HG--
rename : src/Pure/System/build.ML => src/Pure/Tools/build.ML
rename : src/Pure/System/build.scala => src/Pure/Tools/build.scala
rename : src/Pure/System/build_dialog.scala => src/Pure/Tools/build_dialog.scala

identify dialogs via official serial and maintain as result message;
clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly;
cumulate_markup/select_markup depending on command state;
explicit Rendering.output_messages;
tuned source structure;

support dialog via document content;

generalized notion of active area, where sendback is just one application;
some support for graphview via active area;

--HG--
rename : src/Pure/PIDE/sendback.ML => src/Pure/PIDE/active.ML
rename : src/Tools/jEdit/src/sendback.scala => src/Tools/jEdit/src/active.scala

some support for ML runtime statistics;

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

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

more abstract Sendback operations, with explicit id/exec_id properties;
purge result messages (again), cf. db58490a68ac, 7b61a539721e;

more friendly handling of Pure.thy bootstrap errors;

separate module Graph_Display;
tuned signature;

added graph encode/decode operations;
tuned signature;

more informative error message from failed goal forks (violating old-style TTY protocol!);

discontinued centralistic changelog;

theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;

clarified bootstrapping of Pure;

more standard Thy_Load.check_thy for Pure.thy, relying on its header;
pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy;
clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

some support for inlining file content into outer syntax token language;

clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;

prefer general Command_Line.tool wrapper (cf. Scala version);

more official command specifications, including source position;

more standard bootstrapping of Pure outer syntax;

added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

some actual build function on ML side;
further imitation of "usedir" shell script;

simplified Poly/ML setup -- 5.3.0 is now the common base-line;

--HG--
rename : src/Pure/ML-Systems/compiler_polyml-5.3.ML => src/Pure/ML-Systems/compiler_polyml.ML
rename : src/Pure/ML/install_pp_polyml-5.3.ML => src/Pure/ML/install_pp_polyml.ML
rename : src/Pure/ML/ml_compiler_polyml-5.3.ML => src/Pure/ML/ml_compiler_polyml.ML

discontinued support for Poly/ML 5.2.1;

made Context_Position independent from Config;

separate module for prover command execution;

basic support for bundled declarations;

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

--HG--
rename : src/Pure/PIDE/isabelle_document.ML => src/Pure/PIDE/protocol.ML
rename : src/Pure/PIDE/isabelle_document.scala => src/Pure/PIDE/protocol.scala

clarified modules;

--HG--
rename : src/Pure/PIDE/isar_document.ML => src/Pure/PIDE/isabelle_document.ML
rename : src/Pure/PIDE/isar_document.scala => src/Pure/PIDE/isabelle_document.scala

rearranged files;

--HG--
rename : src/Pure/General/isabelle_markup.ML => src/Pure/PIDE/isabelle_markup.ML
rename : src/Pure/General/isabelle_markup.scala => src/Pure/PIDE/isabelle_markup.scala
rename : src/Pure/General/markup.ML => src/Pure/PIDE/markup.ML
rename : src/Pure/General/markup.scala => src/Pure/PIDE/markup.scala

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

added ML antiquotation @{attributes};

discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);

abstract System_Channel in ML (cf. Scala version);
back to TextIO for fifo, which is more stable in Poly/ML 5.4.x;
explicit block buffering -- BinIO might be subject to old Poly/ML defaults;

slightly more general Socket_IO as part of Pure;

--HG--
rename : src/Tools/WWW_Find/socket_util.ML => src/Tools/WWW_Find/server_socket.ML

moved XML/YXML to src/Pure/PIDE;
tuned comments;

--HG--
rename : src/Pure/General/xml.ML => src/Pure/PIDE/xml.ML
rename : src/Pure/General/xml.scala => src/Pure/PIDE/xml.scala
rename : src/Pure/General/yxml.ML => src/Pure/PIDE/yxml.ML
rename : src/Pure/General/yxml.scala => src/Pure/PIDE/yxml.scala

explicit markup for legacy warnings;

more systematic handling of parallel exceptions;
distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

provide node header via Scala layer;
clarified node edit Clear: retain header information;
run_command: node info via document model, error handling within transaction;
node names without ".thy" suffix, to coincide with traditional theory loader treatment;

old term operations are legacy;

moved old code generator to src/Tools/;

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

modernized file proof_checker.ML;

--HG--
rename : src/Pure/Proof/proofchecker.ML => src/Pure/Proof/proof_checker.ML

explicit structure ML_System;
tunned ML bootstrap;

moved bash operations to Isabelle_System (cf. Scala version);

more general bash_process, which allows to terminate background processes as well;

recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;

sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;

XML.pretty with depth limit;

discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;

tuned XML modules;

JVM method invocation service via Scala layer;

some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;

XML data representation of lambda terms;

moved Outer_Syntax.load_thy to Thy_Load.load_thy;
tuned signatures;
tuned module dependencies;

prefer Synchronized.var;

print Path.T with some markup;

clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;

railroad diagrams in LaTeX as document antiquotation;

split Type_Infer into early and late part, after Proof_Context;
added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

provide structure Syntax early (before structure Type), back-patch check/uncheck later;

tuned signature, disentangled dependencies;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
clarified Syntax.root;

--HG--
rename : src/Pure/Syntax/syn_ext.ML => src/Pure/Syntax/syntax_ext.ML

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

separate structure Term_Position;
dismantled remains of structure Type_Ext;

renamed Standard_Syntax to Syntax_Phases;

--HG--
rename : src/Pure/Syntax/standard_syntax.ML => src/Pure/Syntax/syntax_phases.ML

separate module for standard implementation of inner syntax operations;

moved Isar/local_syntax.ML to Syntax/local_syntax.ML;

--HG--
rename : src/Pure/Isar/local_syntax.ML => src/Pure/Syntax/local_syntax.ML

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

discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;

clarified bootstrapping of structure TimeLimit;

--HG--
rename : src/Pure/ML-Systems/time_limit.ML => src/Pure/Concurrent/time_limit_dummy.ML

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

--HG--
rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML

removed bash from ML system bootstrap, and past the Secure ML barrier;

--HG--
rename : src/Pure/ML-Systems/bash.ML => src/Pure/Concurrent/bash_sequential.ML

more explicit Isabelle_System operations;

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

simplified some internal flags using Config.T instead of full-blown Proof_Data;

load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

removed ancient constdefs command

eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;

more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

recognize more "smlnj" variants;

moved Isar_Document to Pure/PIDE;

--HG--
rename : src/Pure/System/isar_document.ML => src/Pure/PIDE/isar_document.ML
rename : src/Pure/System/isar_document.scala => src/Pure/PIDE/isar_document.scala

discontinued support for Poly/ML 5.0 and 5.1 versions;

added functor Linear_Set, based on former adhoc structures in document.ML;
Linear_Set.delete_after (ML): actually delete table entries;
Scala Linear_Set: clarified exceptions, according to ML version;
simplified Document.node using Linear_Set;
ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;

more explicit / functional ML version of document model;
tuned;

moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;

more convenient split of class modules: class and class_declaration

--HG--
rename : src/Pure/Isar/class_target.ML => src/Pure/Isar/class.ML
rename : src/Pure/Isar/class.ML => src/Pure/Isar/class_declaration.ML

renamed Theory_Target to the more appropriate Named_Target

--HG--
rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML

moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order

Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;

type XML.body as basic data representation language;
tuned;

split off structure Generic_Target into separate file

simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;

moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;

removed legacy aliases;

uniform ML environment setup for Isar and PG;

keep structure ThyLoad for the sake of Proof General;

modernized some structure names, keeping a few legacy aliases;

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

do not open Legacy by default;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;

--HG--
rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML

centralized legacy aliases;

renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

--HG--
rename : src/Pure/Isar/spec_parse.ML => src/Pure/Isar/parse_spec.ML

renamed structure ValueParse to Parse_Value;
eliminated old-style structure alias V;

--HG--
rename : src/Pure/Isar/value_parse.ML => src/Pure/Isar/parse_value.ML

renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

--HG--
rename : src/Pure/Isar/outer_keyword.ML => src/Pure/Isar/keyword.ML
rename : src/Pure/Isar/outer_parse.ML => src/Pure/Isar/parse.ML

slightly more logical bootstrap order -- also helps to sort out proof terms extension;

added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
added ProofContext.read_type_name_proper;
localized ProofContext.read_class/read_arity/cert_arity;
localized ProofContext.class_space/type_space etc.;

Digesting strings according to SHA-1.

separate structure Typedecl;

explicit representation of single-assignment variables;

setup for official Poly/ML 5.3.0, which is now the default;

--HG--
rename : src/Pure/ML-Systems/polyml.ML => src/Pure/ML-Systems/polyml-5.2.ML
rename : src/Pure/ML-Systems/polyml-experimental.ML => src/Pure/ML-Systems/polyml.ML

Rules that characterize functional/relational specifications.

Concurrently cached values.

more official status of sequential implementations;
tuned;

--HG--
rename : src/Pure/Concurrent/par_list_dummy.ML => src/Pure/Concurrent/par_list_sequential.ML
rename : src/Pure/Concurrent/synchronized_dummy.ML => src/Pure/Concurrent/synchronized_sequential.ML

separate concurrent/sequential versions of lazy evaluation;
lazy based on future avoids wasted evaluations;

--HG--
rename : src/Pure/General/lazy.ML => src/Pure/Concurrent/lazy.ML

explicit indication of Unsynchronized.ref;

Dummy version of state variables -- plain refs for sequential access.

clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;

renamed structure Display_Goal to Goal_Display;

--HG--
rename : src/Pure/display_goal.ML => src/Pure/goal_display.ML

renamed Pure/tctical.ML to Pure/tactical.ML;

--HG--
rename : src/Pure/tctical.ML => src/Pure/tactical.ML

moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;

Support for copy-avoiding functions on pure values, at the cost of readability.

moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);

just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;

early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
late setup of ML_Env and ML_Compiler;

added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);

slightly later setup of ML and secure operations;

tuned comments;

ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;

turned structure NetRules into general Item_Net, which is loaded earlier;

--HG--
rename : src/Pure/Isar/net_rules.ML => src/Pure/item_net.ML

Merge.

moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);

--HG--
rename : src/Pure/Tools/isabelle_process.ML => src/Pure/System/isabelle_process.ML
rename : src/Pure/Tools/isabelle_process.scala => src/Pure/System/isabelle_process.scala
rename : src/Pure/Isar/isar.ML => src/Pure/System/isar.ML
rename : src/Pure/Isar/session.ML => src/Pure/System/session.ML

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

added old_term.ML;

moved value.ML to src/Tools

cleaned up binding module and related code

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML

added context_position.ML;

removed deriv.ML which is now incorporated into thm.ML;

added deriv.ML: Abstract derivations based on raw proof terms.

separate Concurrent/ROOT.ML;

added Concurrent/task_queue.ML;

added Concurrent/future.ML;

added Concurrent/mailbox.ML;

added Concurrent/schedule.ML;

structure Distribution: swapped default for is_official;

tuned order

load type_infer.ML after Syntax module;

load proof term operations later;

removed obsolete compress.ML

removed obsolete fact_index.ML;
added facts.ML;

tuned structure Distribution;

more elaborate structure Distribution (filled-in by makedist);

removed obsolete context_position.ML (superseded by Position.thread_data);

removed obsolete banner;

removed typedecl.ML (cf. object_logic.ML);

separated typedecl module, providing typedecl command with interpretation

load axclass.ML before Isar;

load variable.ML before conv.ML;

added interpretation.ML;

moved ML_XXX.ML files to Pure/ML;

codegen.ML is now loaded in Pure again.

tuned order;

use logic.ML earlier;
added primitive_defs.ML;

added Syntax/simple_syntax.ML;

renamed config_option.ML to config.ML;

use config_option.ML after sign.ML;

renamed config.ML to config_option.ML;

added config.ML;

simplified loading of ML files -- no static forward references;

use position.ML earlier;

use position.ML after pretty.ML;

added context_position.ML;

added conv.ML;

renamed some old names Theory.xxx to Sign.xxx;

load type_infer.ML early;

removed Pure/Syntax/ROOT.ML;

added print_mode (generic non-sense);

added more_thm.ML;

load morphism.ML later;

tuned order;

removed obsolete proof_general.ML;

Enable new Proof General code again after SML/NJ compatibility fixes by Florian.

Disable new Proof General code until SML/NJ compile fixed.

Use new Proof General code by default [see comment for reverting]

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

reorganized structure Tactic vs. MetaSimplifier;

reorganized structure Goal vs. Tactic;

Build instructions for new Proof General module [not yet activated]

added morphism.ML, General/ml_syntax.ML;

added General/basics.ML;

added Pure/term_subst.ML;

added Pure/assumption.ML;

added Pure/subgoal.ML;

added name.ML;

added variable.ML;

removed IsaPlannner things from Pure. Moved to Provers.

tuned;

added conjunction.ML;

moved theory presentation to Isar/ROOT.ML;

use axclass.ML earlier (in Isar/ROOT.ML);

use proof_general.ML: setmp quick_and_dirty captures default value;

load envir.ML and logic.ML early;

tuned comments;

CPure: Context.add_setup;

added modules for code generator generation two, not operational yet

added consts.ML;

added goal.ML;
moved use of goals.ML;

removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;

added quick_and_dirty (from Isar/skip_proofs.ML);

removed obsolete BasisLibrary;
proof_general.ML: setmp proofs 1 to capture sane default preferences;

added compress.ML;

tuned;

- introduce Pure/Tools directory
- add compute oracle to Pure/Tools

removed Pure/theory_data.ML;

Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).

added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;

superceded by Pure.thy and CPure.thy;

Debugging code (error_depth) removed.

First version of global registration command.

the new subst tactic, by Lucas Dixon

Merging the meta-simplifier with the Provers-simplifier. Next step:
make the simplification procedure simpset-aware.

moved print_mode to General/output.ML; load General/pretty.ML early;

type.ML now before Syntax module;

Added program extraction module.

added fact_index.ML;

Interface/proof_general.ML move to proof_general.ML;

print_depth 10;

tuned;

print_depth 8 from the very beginning;

reorganize sources to accomodate locales;

revert to proper version (!);

added object_logic.ML;

final proofs := 0;

Added new files for proof terms.

fixed version string;

removed Session.finish ();

Added new file meta_simplifier.ML

"Isabelle repository version";

quick_and_dirty moved to Isar/skip_proof.ML;

activate ml_prompts;

renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;

added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;

axclass.ML loaded after Isar;

Session.finish ();
use;

use, cd;

tuned;

moved print_mode to ROOT.ML

removed attribute.ML;

String added to BasisLibrary

added Isar;

structure Hidden = struct end;

added Real to BasisLibrary

added Int to BasisLibrary

added locale.ML;

late setup of Pure and CPure;

tuned comment;

added quick_and_dirty flag;

moved actual (C)Pure theories to pure.ML;

moved table.ML, object.ML, seq.ML, name_space.ML to General;

added theory_data.ML;

added object.ML;

tuned msgs;

version under control of Admin/makedist;
ml_prompts;

global_names moved to pure_thy.ML;

tuned comments;

added attribute.ML;

tuned comment;

replaced symtab.ML by table.ML;

tuned;

version = "Isabelle98: Jan 1998";

moved global_names ref to Pure/ROOT.ML;

tuned;

changed Sequence interface (now Seq, in seq.ML);

removed data.ML (made part of sign.ML);

structure BasisLibrary;

added pure_thy.ML;

tuned;

added data.ML;

added name_space.ML;

removed init_database;

set version;

added sorts.ML, type_infer.ML;

cd made readably again;

Uses Basis Library equivalent of cd

Updated version and date

Increased revision number

Now loads deriv.ML

Updated for new file search.ML

Theories are now in theory.ML

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

New version number

Now loads symtab.ML before term.ML. Functor
> SymtabFun has been changed to the structure Symtab.

updated version number to revision 4

Added

functor f() = struct end

to hide functors to save space.

updated version

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

Updated the "version" variable (which was never done for
Isabelle-94 revisions 1 and 2!)

AxClass no longer open;

added init_database (somewhat experimental);

updated the identifier "version"

added "axclass.ML", structure AxClass;

updated version to October 93

delete_file now has type string -> unit in both NJ and POLY,
use of Pure/Thy/ROOT has been moved to the end of Pure/ROOT again

Pure/ROOT.ML
cleaned comments;
removed extraneous 'print_depth 1';
replaced Basic_Syntax by BasicSyntax
added 'use "install_pp.ML"';

Pure/README
fixed comments;

Pure/POLY.ML
Pure/NJ.ML
make_pp: added fbrk;

Pure/install_pp.ML
replaced "Ast" by "Syntax";

Pure/sign.ML
added 'quote' to some error msgs;

moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm

Initial revision