future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;

uniform ml_prompts for RAW and Pure;

eliminated old Addsimps;

Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;

fixed possibility_tac;

eliminated global SIMPSET, CLASET etc. -- refer to explicit context;

merged

merged

split_codegen now eta-expands terms on-the-fly.

proper context for prove_cont/adm_tac;

with_attributes: canonical capture/release scheme (potentially iron out race condition);

considerable speedup of benchmarks by using minimal simpset;

allow non-printable symbols within string tokens;

merged

add lemma det_diagonal; remove wellorder requirement on several lemmas

merged

tuned some theorem and attribute bindings

proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;

eval_antiquotes: joint scanning of ML tokens and antiquotations;

added scan_antiq; more robust scan_ml: plain scanning without cut, regular Symbol_Pos.content instead of Symbol_Pos.implode (which contains spurious Symbol.DEL is used with proper positions);

RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);

added tokenize; internal scan_str: ensure Symbol.is_regular, otherwise it might swallow the stopper and crash!

parameterized datatype antiquote and read operation;

Antiquote.Text: keep full position information;

OuterLex.read_antiq;

moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;

moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML; scan_comment: recovered change_prompt; moved read_antiq to outer_lex.ML;

use Name.of_binding for basic logical entities without name space (fixes, case names etc.);

Name.of_binding: proper full_name (with checks) before projecting base name;

merged

imported patch euclidean

Merged.

Updated chapters 1-5 to locale reimplementation.

command 'use', 'ML': apply ML environment to theory and target as well; tuned command descriptions;

added map_contexts (cf. Proof.map_contexts);

tuned;

generalized ML_Context.inherit_env;

more precise type Symbol_Pos.text;

more precise type Symbol_Pos.text; geralized ML_Context.inherit_env;

de-camelized Symbol_Pos;

Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;

reduced verbosity;

made SML/NJ happy

tuned interpunctation

strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions);

close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;

reverted abbreviations: improved performance via Item_Net.T;

export match_rew -- useful for implementing "procs" for rewrite_term;

tuned comment;

merged

document new additions to HOL/Library

clean up proofs

adapted to general Item_Net;

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

renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);

goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;

eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly; tuned;

tuned aeconv: test plain aconv before expensive eta_contract;

substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);

refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;

provide Simplifier.norm_hhf(_protect) as regular simplifier operation;

method parser: pass proper context;

merged

simplified method setup;

updated generated file;

simplifief 'method_setup' command;

spelling;

export method parser;

adapted 'method_setup' command to Method.setup;

tuned signature;

have remote script interrupted like the other provers

simplified method setup;

export section, sections; tuned signature;

merged

updated NEWS

use goal instead of Proof State

split relevance-filter and writing of problem-files; perform relevance-filtering for only one subgoal; added additional explicit timeout to provers

show certain errors to the user

removed connection check; adapted times

merged

merged

reverted to old version of Set.thy -- strange effects have to be traced first

simplified attribute and method setup;

simplified attribute setup; replaced add_args by add parser;

simplified attribute setup;

updated generated files;

added 'attribute_setup' command;

added setup and attribute_setup -- expect plain parser instead of syntax function; aded add_del parser;

ML_Syntax.make_binding;

added make_binding;

removed obsolete no_base_names naming policy;

merged

merged

coherent binding policy with primitive target operations

moved some generic nonsense to arith_data.ML

tuned ML code

remove legacy ML bindings

simplified method setup;

simplified goal_spec: default to first goal;

eliminated type Args.T; pervasive types 'a parser and 'a context_parser;

added simplified setup; eliminated type Args.T; pervasive types 'a parser and 'a context_parser;

pervasive types 'a parser and 'a context_parser;

unified type Proof.method and pervasive METHOD combinators;

more regular method setup via SIMPLE_METHOD;

tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;

merged

fix typed print translation for CARD('a)

introduce new helper functions; clean up proofs

merged

added comment

hiding numeric coercions in LaTeX

merged

dropped spurious `quote` tags

merged

tuned

strippd Id

vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement

tuned

consider exit status of code generation direcitve

provide regular ML interfaces for Isar source language elements;

get data from plain Proof.context;

more user aliases;

merged

remove trailing spaces

remove trailing spaces

simplified preparation and outer parsing of specification; export extern cmd interfaces as well;

simplified preparation and outer parsing of specification;

removed legacy_infer_term, legacy_infer_prop; modernized naming conventions: foo vs. foo_cmd; simplified preparation and outer parsing of specification; simplified command syntax setup;

old name_spec for 'axioms' and 'defs' (from spec_parse.ML);

added legacy type inference (from fixrec_package.ML);

simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements; simplified check_specification, read_specification: operate on a single list of simultaneous statements; tuned;

removed old named_spec, spec_name, spec_opt_name; clarified spec vs. specs; added alt_specs, where_alt_specs -- try to be robust against malformed input;

keep dead code fresh;

tuned;

merged

merged

added div lemmas

merged

optional latex sugar

Assumption.all_prems_of, Assumption.all_assms_of;

Assumption.local_prems_of;

renamed assms_of to all_assms_of, and prems_of to all_prems_of; added local_assms_of, local_prems_of; removed unused add_view;

axiomatization: more precise treatment of binding;

renamed sticky_prefix to mandatory_path;

replaced old-style add_path/no_base_names by sticky_prefix;

updated according to actual manual title;

renamed NameSpace.bind to NameSpace.define;

renamed bind to define; misc tuning and polishing;

tuned signature;

updated generated files;

tuned;

added 'local_setup' command; tuned;

debugging: special handling of EXCURSION_FAIL;

tuned;

delete unused generated files;

basic setup for "main" as generated Isabelle manual;

tuned;

merged

merged

fixed typo

(restored previous version)

corrected type inference of primitive definitions

HOLogic.mk_set, HOLogic.dest_set

tuned

tuned funny error message

stripped dead code

min_weak_def [code del]

renamed (unused?) "split.splits" to split_splits -- it was only accepted by accident;

merged

Extended approximation boundaries by fractions and base-2 floating point numbers

Added "What's in Main" to doc sources

merged

Docs

Updated paths in Decision_Procs comments and NEWS

eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);

more precise treatment of qualified bindings; tuned;

removed obsolete absolute_path -- use root_path with qualified binding;

explicit Binding.qualified_name -- prevents implicitly qualified bstring;

Thm.def_binding_optional;

added def_binding_optional -- robust version of def_name_optional for bindings;

merged

avoid inspecting pretty output

explicit code equations for some rarely used pred operations

moved Decision_Procs examples to Decision_Procs/ex

explicitly delete some code equations

delete code equations for types pred and seq

merged

Docs

Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;

recover old ids;

controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;

explicit root_path, parent_path; derived absolute_path; tuned;

removed obsolete no_base_names; tuned;

invoke_case: proper qualification of name binding, avoiding old no_base_names;

add_path: discontinued special meaning of "//", "/", ".."; added root_path, parent_path;

merged

Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

Instead of giving up entirely, arith now ignores all inequalities when there are too many.

merged

Fixed type error which appeared when Approximation bounds where specified as floating point numbers

just one naming policy based on binding content -- eliminated odd "object-oriented" style; uniform handling of regular vs. mandatory name prefixes -- add_path and sticky_prefix may be freely intermixed; misc tuning and cleanup;

tuned proofs; tuned document;

added qualified_name_of; tuned;

pretty_full_theory: no longer display name prefix -- naming is far more complex now;

quote binding for ML toplevel pp;

merged

Instead of giving up entirely, arith now ignores all inequalities when there are too many.

updated generated file -- changed due to different treatmeant of type constraints in OptionalSugar.thy;

more robust treatment of (authentic) consts within translations;

Docs

merged

Docs

added session HOL-Docs;

tuned;

simplified presentation_context_of;

markup antiquotation options; more correct references to external manuals;

fornal markup for antiquotation options;

* More systematic treatment of long names, abstract name bindings, and name space operations. * Simplified interface for defining document antiquotations via ThyOutput.antiquotation.

moved @{ML_functor} and @{ML_text} to Pure; adapted to simplified ThyOutput.antiquotation interface; misc tuning;

replaced old locale option by proper "text (in locale)";

adapted to simplified ThyOutput.antiquotation interface; fixed theory name;

adapted to simplified ThyOutput.antiquotation interface;

simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output; removed incomprehensible args parser setup; removed obsolete locale flag -- text is already localized; misc tuning and cleanup of concrete antiquotations; goal state antiquotations: ignore source flag;

merged

merged

NameSpace.base_name ~> Long_Name.base_name

Docs

merged

fixed typing of UN/INT syntax

more contributors;

adapted ThyOutput.antiquotation;

refined antiquotation interface: formally pass result context and (potential) result source; removed redundant raw_antiquotation;

merged

binding replaces bstring

dropped eq_pred

merged

refined enumeration implementation

added top and bot syntax

added predicate compiler, as formally checked prototype, not as user package

attempt to bypass spurious infix syntax problem on polyml/sun