2009-03-11 wenzelm 2009-03-11 more precise treatment of qualified bindings; tuned;
2009-03-11 wenzelm 2009-03-11 removed obsolete absolute_path -- use root_path with qualified binding;
2009-03-11 wenzelm 2009-03-11 explicit Binding.qualified_name -- prevents implicitly qualified bstring;
2009-03-11 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-11 wenzelm 2009-03-11 added def_binding_optional -- robust version of def_name_optional for bindings;
2009-03-11 haftmann 2009-03-11 merged
2009-03-11 haftmann 2009-03-11 avoid inspecting pretty output
2009-03-11 haftmann 2009-03-11 explicit code equations for some rarely used pred operations
2009-03-11 haftmann 2009-03-11 moved Decision_Procs examples to Decision_Procs/ex
2009-03-11 haftmann 2009-03-11 explicitly delete some code equations
2009-03-11 haftmann 2009-03-11 delete code equations for types pred and seq
2009-03-10 wenzelm 2009-03-10 merged
2009-03-10 nipkow 2009-03-10 Docs
2009-03-10 wenzelm 2009-03-10 Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
2009-03-10 wenzelm 2009-03-10 recover old ids;
2009-03-10 wenzelm 2009-03-10 controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;
2009-03-10 wenzelm 2009-03-10 explicit root_path, parent_path; derived absolute_path; tuned;
2009-03-10 wenzelm 2009-03-10 removed obsolete no_base_names; tuned;
2009-03-10 wenzelm 2009-03-10 invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-10 wenzelm 2009-03-10 add_path: discontinued special meaning of "//", "/", ".."; added root_path, parent_path;
2009-03-10 wenzelm 2009-03-10 merged
2009-03-10 webertj 2009-03-10 Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-10 webertj 2009-03-10 Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-10 wenzelm 2009-03-10 merged
2009-03-10 hoelzl 2009-03-10 Fixed type error which appeared when Approximation bounds where specified as floating point numbers
2009-03-10 wenzelm 2009-03-10 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;
2009-03-10 wenzelm 2009-03-10 tuned proofs; tuned document;
2009-03-10 wenzelm 2009-03-10 added qualified_name_of; tuned;
2009-03-10 wenzelm 2009-03-10 pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-10 wenzelm 2009-03-10 quote binding for ML toplevel pp;
2009-03-10 wenzelm 2009-03-10 merged
2009-03-10 webertj 2009-03-10 Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-10 wenzelm 2009-03-10 updated generated file -- changed due to different treatmeant of type constraints in OptionalSugar.thy;
2009-03-10 wenzelm 2009-03-10 more robust treatment of (authentic) consts within translations;
2009-03-09 nipkow 2009-03-09 Docs
2009-03-09 nipkow 2009-03-09 merged
2009-03-09 nipkow 2009-03-09 Docs
2009-03-09 wenzelm 2009-03-09 added session HOL-Docs;
2009-03-09 wenzelm 2009-03-09 tuned;
2009-03-09 wenzelm 2009-03-09 simplified presentation_context_of;
2009-03-09 wenzelm 2009-03-09 markup antiquotation options; more correct references to external manuals;
2009-03-09 wenzelm 2009-03-09 fornal markup for antiquotation options;
2009-03-09 wenzelm 2009-03-09 * More systematic treatment of long names, abstract name bindings, and name space operations. * Simplified interface for defining document antiquotations via ThyOutput.antiquotation.
2009-03-09 wenzelm 2009-03-09 moved @{ML_functor} and @{ML_text} to Pure; adapted to simplified ThyOutput.antiquotation interface; misc tuning;
2009-03-09 wenzelm 2009-03-09 replaced old locale option by proper "text (in locale)";
2009-03-09 wenzelm 2009-03-09 adapted to simplified ThyOutput.antiquotation interface; fixed theory name;
2009-03-09 wenzelm 2009-03-09 adapted to simplified ThyOutput.antiquotation interface;
2009-03-09 wenzelm 2009-03-09 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;
2009-03-09 wenzelm 2009-03-09 merged
2009-03-09 haftmann 2009-03-09 merged
2009-03-09 haftmann 2009-03-09 NameSpace.base_name ~> Long_Name.base_name
2009-03-09 nipkow 2009-03-09 Docs
2009-03-09 nipkow 2009-03-09 merged
2009-03-09 nipkow 2009-03-09 fixed typing of UN/INT syntax
2009-03-09 wenzelm 2009-03-09 more contributors;
2009-03-09 wenzelm 2009-03-09 adapted ThyOutput.antiquotation;
2009-03-09 wenzelm 2009-03-09 refined antiquotation interface: formally pass result context and (potential) result source; removed redundant raw_antiquotation;
2009-03-09 haftmann 2009-03-09 merged
2009-03-09 haftmann 2009-03-09 binding replaces bstring
2009-03-09 haftmann 2009-03-09 dropped eq_pred