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;

added const_binding;

added prefix_name, suffix_name; added eq_name; added opaque signature constraint to prevent accidental equality test;

Theory.add_axioms/add_defs: replaced old bstring by binding;

renamed rep_ss to MetaSimplifier.internal_ss;

Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;

oracle: proper name position, tuned;

merged

drop poisonous code equations

suppress document output

theory with syntax for lattice operations

added babel -- necessary for bind infix syntax

added enumeration of predicates

moved instance option :: finite to Option.thy

constructive version of Cantor's first diagonalization argument

equalities for Min, Max

merged

added lemma

merged

Docs

eliminated Output.immediate_output -- violates the official message channel protocol;

schedule_seq: handle after_load errors as in schedule_futures;

replaced archaic use of rep_ss by Simplifier.mksimps;

improved error handling for document antiquotations;

merged

merged

Added "expect" option to Refute, like in Nitpick, that allows to write regression tests. Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha).

added lemmas

Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead. I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed).

merged

merged

Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.

merged

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

tuned

moved complete_lattice to Set.thy

dropped Id

corrected slip in NEWS

merged

added strict_mono predicate

Identifiers of some old CVS file versions;

recovered generated files;

more precise deps;

merged

Added Docs

render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;

removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;

removed unused TableFun().fold_map and GraphFun().fold_map_nodes;

removed spurious occurrences of old rep_ss;

Thm.add_oracle interface: replaced old bstring by binding;

silent chmod;

Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;

close_schematic_term: uniform order of types/terms; tuned;

eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;

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

fixed proofs -- follow-up to ecd6f0ca62ea;

renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name"); tuned;

renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;

eliminated obsolete ProofContext.full_bname;

Binding.prefix_of;