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