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

remove duplicate [algebra] declarations

generalize more div/mod lemmas

generalize some theorems about div/mod

updated to jedit-4.5.1;

merged

note a code eqn in quotient_def

dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct

more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)

fixed eta-extension of higher-order quantifiers in THF output

renamed "smt_fixed" to "smt_read_only_certificates"

tuning

tuning (in particular, Symtab instead of AList)

tweak slices, based on eval by Daniel Wand

be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)

print a hint

avoid DL

TFF: declare free types as types

merged

association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements

remove redundant lemmas

move int::ring_div instance upward, simplify several proofs

rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names

extend definition of divmod_int_rel to handle denominator=0 case

tuned proofs

shorten a proof

simplify some proofs

rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.

simplify some proofs

merged

merged

reverted to canonical name

merged

merged

revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda

merged

fix incorrect code_modulename declarations

code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)

remove old-style semicolon

merged

Functions and lemmas by Christian Sternagel

more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;

disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;

tuned comment

merged

merged

tuned proof - no smt call

more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);

updated theory header syntax and related details;

ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE); update for prospective jdk1.7.x component;

merged

reintroduced broken proofs and regenerated certificates

merged, resolving trivial conflict;

fixed Nitpick after numeral representation change (2a1953f0d20d)

merged fork with new numeral representation (see NEWS)

merged

use Thm.transfer for thms stored in generic context data storage

hide invariant constant

explicit SMTP server (appears to be required after recent change of system configuration);

more isatest subscribers;