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

UN syntax fix

merged

Docs updates

use simplified ThyOutput.antiquotation; eliminated obscure structure alias;

added (raw_)antiquotation -- simplified wrapper for defining output commands;

simplified presentation: pass state directly;

simplified presentation: built into transaction, pass state directly;

adapted to structure Long_Name;

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

proper local context for text with antiquotations;

more explicit warning message;

added qualified_name -- emulates old-style qualified bstring; tuned;

added General/long_name.ML;

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

index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;

proper context for Simplifier.pretty_ss;

added dest_ss; proper context fo pretty_ss; tuned;

use binding type;

merged

merged

restructured theory Set.thy

merged

Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.

Added a second timeout mechanism to Refute. For some reason, TimeLimit.timeLimit often does not work, and it leaves Refute running forever, making any evaluation using Mutabelle or Mirabelle impossible. The redundant timeout seems to do the trick.

merged

Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.

minimal adaptions for abstract binding type;

more uniform handling of binding in packages;

more uniform handling of binding in targets and derived elements;

replace old bstring by binding for logical primitives: class, type, const etc.;

moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;

adapted Syntax.const_name;

canonical argument order for type_name, const_name;