removed obsolete isar-overview manual;

dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret

merged

rudimentary handling of products in finitize_functions in Quickcheck-Narrowing

improved equality check for modes in predicate compiler

rename ML structure to avoid shadowing earlier name

add type annotations to make SML happy (cf. ec6187036495)

merged

new transfer proof method

renamed Tools/transfer.ML to Tools/legacy_transfer.ML

prefer prog-prove, suppress isar-overview;

merged

merged

formal integration of "prog-prove" manual; "main" is a reference manual;

prefer static dependencies;

merged

modernized obsolete old-style theory name with proper new-style underscore

removed use of CharVector in generated parser, to make SMLNJ happy

avoid duplicate PIDE markup; tuned;

less intrusive visibility;

more robust re-import wrt. non-HHF assumptions;

consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;

close context elements via Expression.cert/read_declaration; ensure visible context;

merged

added me to isatest email list

new package Lifting - initial commit

add floor/ceiling lemmas suggested by René Thiemann

made sure that " is shown in tutorial text

merged

tuned proofs

merged

towards showing " in the tutorial

tuned proof in order to avoid warning message

remove unnecessary qualifiers on names

add lemma Suc_1

merged

Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information

normalize defs (again, cf. 008b7858f3c0);

some context examples;

retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;

another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

more uniform abbrev vs. define;

tuned;

clarified generic_const vs. close_schematic_term;

tuned;

more uniform theory_abbrev with const_declaration;

avoid const_declaration in aux. context (cf. locale_foundation);

clarified background_foundation vs. theory_foundation (with const_declaration);

tuned;

more general standard_declaration; generic const declaration, which is applied to nested targets (named target only);

better restore after close_target;

tuned;

clarified standard_declaration vs. theory_declaration;

smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);

tuned;

tuned;

tuned signature;

misc tuning and simplification;

better restore to first target, not last target;

refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);

more general Local_Theory.restore, allow any nesting level;

new tutorial

New manual Programming and Proving in Isabelle/HOL

add simp rules for dvd on negative numerals

merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)

clarified terminology; added reference to bundle component

less modest NEWS; CONTRIBUTORS

renamed import session back to Import, conforming to directory name; NEWS

more precise IsaMakefile (eg. see HOL-Algebra);

more keywords;

merged

merged

removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare

Modernized HOL-Import for HOL Light

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);