modernized notation -- to make it work for authentic syntax;

proper markup of const syntax;

more precise dependencies;

added lemma

moved reduced Induct/SList back from AFP.

adjusted to changes in cs b987b803616d

disabled some old (fragile) isatests;

tuned settings; activated kodkodi, i.e. HOL-Nitpick_Examples;

fixed document;

eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;

made SML/NJ happy;

tuned;

authentic term syntax; more precise treatment of naming vs. binding; misc tuning;

Thm.def_binding;

moved ancient Drule.get_def to OldGoals.get_def;

quote the constant and theorem name with @{text}

merged

merged

local Simplifier.context; tuned tactic setup;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

tuned message;

Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;

merged

context theorem is optional

added dest_comb

a simple concept for datatype invariants

using Code.bare_thms_of_cert

simplified

added code_abstype keyword

Initial version of HOL quotient package.

merge

added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

fix bug in Nitpick's monotonicity code w.r.t. binary integers

merged

merged

get rid of many duplicate simp rule warnings

get rid of warnings about duplicate simp rules in all HOLCF theories

HOLCF-FOCUS depends on ex/Stream.thy

fix looping call to simplifier

merged

Use top-down rewriting to contract abbreviations.

Added function rewrite_term_top for top-down rewriting.

merged

added lemma

merged

tuned isatest settings;

removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;

locale: more precise treatment of naming vs. binding;