more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);

more explicit isatest environment settings (from private .bashrc);

merged

fix search-and-replace errors

move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy

add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral

move lemmas from Nat_Numeral.thy to Nat.thy

move lemmas from Nat_Numeral to Int.thy and Num.thy

merged

adding theory to prove completeness of the exhaustive generators

refine bindings in quickcheck_common: do not conceal and do not declare as simps

hiding fact not so aggressively

power on predicate relations

made Mirabelle-SH's 'trivial' check optional;

merged

more specific notion of partiality (cf. Scala version);

use qualified names for rsp and rep_eq theorems in quotient_def

announcing NEWS (cf. 446cfc760ccf)

remove obsolete simp rule for powers

remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}

remove unneeded rewrite rules for powers of numerals

remove duplicate lemma Suc_numeral

move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy

bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy

educated guess to include jdk

improved robustness with new antiquoation by Makarius

merged

updates

updated documentation files (cf. c14fda8fee38)

clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME; clarified jEdit/README_BUILD;