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;