merged

adapted Mira configuration to dd04c8173bb2.

removed Nat_Numeral.thy, moving all theorems elsewhere

less brutal return from function, to allow caller to report error;

more general context command with auxiliary fixes/assumes etc.;

more precise type annotation (cf. 6523a21076a8);

nothing specific about named target;

clarified Generic_Target.notes: always perform Attrib.partial_evaluation; more uniform Generic_Target.theory_notes/locale_notes: apply facts to all target contexts;

added Attrib.global_notes/local_notes/generic_notes convenience;

simplified;

tuned signature;

clarified Named_Target.target_declaration: propagate through other levels as well; tuned signature;

Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom; Local_Theory.target refers to bottom; tuned signature;

tuned proofs

merged

tuned proof

add lemma power_le_one

tuned;

tuned signature;

more direct Local_Defs.contract; eliminated slightly odd Local_Defs.trans_term/trans_prop;

more precise Local_Defs.expand wrt. *local* prems only;

tuned comment;

more robust Scala 2.9.x interpreter invocation -- avoid separate interpreter thread and thus deadlock of Swing_Thread.now;

tuned;

dropped empty files

dropped now obsolete Cset theories

merged

tuned proofs, less guesswork;

merged

load Tools/numeral.ML in Num.thy

tuned proof

set up numeral reorient simproc in Num.thy

remove redundant simp rule

add simp rules for eve/odd on numerals

remove content-free theory ex/Arithmetic_Series_Complex.thy

rephrase lemmas about arithmetic series using numeral '2'

rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'

replace lemmas eval_nat_numeral with a simpler reformulation

restate various simp rules for word operations using pred_numeral

new lemmas for simplifying subtraction on nat numerals

removed redundant nat-specific copies of theorems

move more theorems from Nat_Numeral.thy to Num.thy

"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);

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;

merged

removed references to obsolete theorems

merged

some tuning while reviewing the current state of the quotient_def package

improving spelling

changing more definitions to quotient_definition

removing now redundant impl_of theorems in DAList

using abstract code equations for proofs of code equations in Multiset

simplified statements and proofs;

tuned whitespace;

updated Sign.add_type, Name_Space.declare;

updated comments;

merged

remove unnecessary rules from the simpset

remove unused premises

remove duplicate lemmas

mark some duplicate lemmas for deletion

remove more redundant lemmas

tuned proofs

remove redundant lemmas

generalized lemma zpower_zmod

remove redundant lemma

remove redundant lemma