read_dimacs_cnf_file can now read DIMACS files that contain successive white-space characters.

Expand nested abbreviations before applying dummy patterns.

Removed eq_to_mono2, added not_mono.

Streamlined setup for monotonicity rules (no longer requires classical rules).

Simplified treatment of monotonicity rules.

removed obsolete test tags;

Added tag Isabelle2009-1 for changeset 6a973bd43949

slightly less ambitious settings, to avoid potential out-of-memory problem;

even higher proof-shell-quit-timeout -- saving main HOL takes 20s on a *fast* machine;

updated date;

more robust treatment of spaces in directory names;

adding subsection about the predicate compiler to the code generator tutorial

Added tag isa2009-1-test for changeset e1c262952b02

updated date;

Expand nested abbreviations before applying dummy patterns.

raised proof-shell-quit-timeout to accomodate bulky write-back images;

deactivated default for E_HOME, SPASS_HOME -- now configured as components; deactivated default for VAMPIRE_HOME -- superceded by remote_vampire;

double check file permissions of write-back image -- more robust for root or administrator on Cygwin;

tuned message;

added HOLCF image;

workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997

updated generated files;

proper quoting of array expansion -- allow spaces in components;

added "sos"; added subgoal focus;

PG version 3.7.1.1;

allow spaces within PROOFGENERAL_EMACS;

allow spaces within command-line arguments;

proper quotes;

more abstract handling of repository name;

more menu entries -- backport from PG 4.0 branch;

re-package Isabelle distribution with add-on components;

fixed csdp output parser

additional menu entries;

Added tag isa2009-1-test for changeset 14ff44e21bec

adhoc delay after font installation -- increases chance that Emacs will actually see them;

implicit font installation for Mac OS;

modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;

patch for the infamous antiquotation font-lock problem of Proof General 3.7.1 with GNU Emacs, cf. http://proofgeneral.inf.ed.ac.uk/trac/ticket/236

refer to isabelle-release branch;

include HOL-SMT keywords;

tuned affiliation;

extended list of HOL-Boogie contributors

only add nat/int conversion rules if necessary

more generic explosion of options (also accept newlines, etc.)

respect "unique" attribute: generate distinctness axioms

fixed arity of some empty relations in Nitpick's Kodkod generator; these previously resulted in Kodkod arity errors (similar to type errors for other logics)

fix soundness bug in "uncurry" option of Nitpick

Added tag isa2009-1-test for changeset 4328de748fb2

some rearangement of load order to keep preferences adjacent -- slightly fragile;

use correct Isabelle version name in README file

remove version number from Nitpick manual

fix soundness bug in Nitpick's Kodkod generator for the relational composition case

merged

generate clearer atom names in Nitpick for types that end with a digit; requested by a user

Added tag isa2009-1-test for changeset 9db7854eafc7

fix soundness bug in Nitpick's handling of negative literals (e.g., -1::rat)

consisten upper/lower case

merge

fixed soundness bug / type error in handling of unpolarized (co)inductive predicates in Nitpick

removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these

fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite

fixed soundness bug in Nitpick's handling of typedefs

multiplatform polyml.tar.gz;

updated keywords;

more tuning for release;

added command 'ProofGeneral.pr' for PG 4.0;

merged

improving the setup for the tabled transitive closure thanks to usage of Andreas Lochbihler

updated for release;

Generated files.

Typos in documenation.

ANNOUNCE

merge

fix Nitpick soundness bugs related to integration (in particular, "code_numeral")

generate arguments of relational composition in the right order in Nitpick

CONTRIBUTORS

merged

tuned NEWS

do not add host suffix -- it is appended by test framework

documented size_change in isar-ref manual

clarified; checked

mentioned method size_change in function tutorial

eliminated dead code and some unused bindings, reported by polyml

fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user

fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type

improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex

fixed error in Nitpick's "star_linear_preds" optimization, which resulted in an ill-typed term; reported by Stefan

merged

more uniform view on various number theory refinement steps

Merged.

Generated latex code.

Updated locale documentation.

made SML/NJ happy;

remove presently unused Isabelle application;

more NEWS, more tuning for release;

misc tuning and updates for official release;

tuned;

updated keywords;

Use less whitespace in documentation.

Publication details and minor correction of the text.

Removed obsolete comment.

Merged.

More tests for locale interpretation.

adapted local theory operations -- eliminated odd kind;

minimal Poly/ML startup script;

explicitly mark some legacy freeze operations;

minimal test of current repository version;

slightly longer log tail;

add explicit platform check to wwwfind tool explicit platform check to avoid calling external programs with strange parameters

adjusted help text

wwwfind support currently for Linux only

make repdef work without (open) option

NEWS: HOLCF changes since the last release

removed hard tabs from text (not pattern);

standardized headers;

provide standard isabelle make targets; slightly more accurate dependencies;

merged

load ML directly into theory Code_Generator (quickcheck also requires this);

made script executable

added NEWS item for wwwfind

WWW_Find component: find_theorems via web browser

merged

merged

Rene tuned proof

example theory for new domain package

thy_decl outer syntax for repdef

merged

nicer warning message for indirect-recursive domain definitions

store map_ID thms in theory data; automate proofs of reach lemmas

add map_ID lemmas

domain_isomorphism package defines combined copy function

merged

added Rene Thiemann's normalize function

added lemma

merged

domain_isomorphism package defines copy functions

copy_of_dtyp uses map table from theory data

Domain.thy imports Representable.thy

fix definitions of copy combinators

clean up indentation; add 'definitional' option flag

rename generated abs_iso, rep_iso lemmas

clean up indentation

add dependency on domain_isomorphism.ML

set up domain_isomorphism package in Representable.thy

automate proofs of map_ID theorems

change Theory.requires

use theory data for REP_simps and isodefl_rules

replace defl_tab and map_tab with theory data

separate conjuncts of isodefl theorem

automate isodefl proof

change example to use recursion with continuous function space

add lemma isodefl_cprod

automate definition of map functions; remove unused code

change naming convention for deflation combinators

add new makefile dependencies

prove isomorphism and isodefl rules

avoid using csplit; define copy functions exactly like the current domain package

merged

remove one_typ and tr_typ; add abs/rep lemmas

automate definition of rep/abs functions

get rid of numbers on thy variables

automate proofs of REP equations

cleaned up; factored out fixed-point definition code

automate solution of domain equations

removed fixme - quick-and-dirty flag is appropriate

use of thm-antiquotation

Added new counterexample generator SML_inductive for goals involving inductive predicates.

Added infrastructure for embedding random data generators into code generated for inductive predicates.

unused_thms: show only results from 'theorem(s)' package (via old-style kinds); misc tuning -- slightly less hermetic names;

future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;

toplevel pretty printer for Synchronized.var;

adapted Local_Theory.define -- eliminated odd thm kind;

Specification.definition: Thm.definitionK marks exactly the high-level end-user result;

Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;

merged

merged

Minor correction

some attempts to improve termination of isatest;

Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS

Renamed vector_less_eq_def to the more usual name vector_le_def.

merged

replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules

concealing internal definitions of primrec specifications

adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler

adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned

check if equations are present for all functions to avoid low-level exception later

anti_sym -> antisym

optionally trace theorems used in proof reconstruction

added arithmetic example using div and mod

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits; the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

merged

comment out debugging code in Nitpick

fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"

made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions

removed "debug := true" that shouldn't have been submitted in the first place

Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)

merged

run Nitpick examples if Kodkodi is available

merged

fixed "expect" of Nitpick examples to reflect latest changes in Nitpick

merged

use SAT solver that's available everywhere for this example

invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script; this requires downloading Kodkodi 1.2.4, or writing a "kodkodi" script that invokes "java de.tum.in.isabelle.Kodkodi.Kodkodi $@"

merged

added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus

change the order in which Nitpick tries SAT solvers; so that the binary JNIs come further down the list and can easily be overridden

Fixed splitting of div and mod on integers (split theorem differed from implementation).

merged

Fixed splitting of div and mod on integers (split theorem differed from implementation).

init_theory: Runtime.controlled_execution for proper exception trace etc.;

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

implicit name space grouping for theory/local_theory transactions;

uniform new_group/reset_group; tuned signature;

eliminated dead code;

generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;

member/cons: slightly more correct treatment of multi-index, notably empty one;

merged

Fixed a typo in a comment.

Fixed a typo in a comment.

merged

A few more lemmas from Jeremy

removed hassize predicate

Added new lemmas to Euclidean Space by Robert Himmelmann

eliminated obsolete thm position stuff;

tuned signature;

guard future proofs by Goal.future_enabled;

further explosion of HOL-Boogie verification conditions

merged

proper purge

dropped obsolete documentation; updated generated sources

merged

removed a few global names in Nitpick (styp, nat_less, pairf)

add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; explicit extraction_expand vs. extraction_expand_def attribute;

axiomatization: declare Spec_Rules, direct result;

use simultaneous Morphics.fact;

primitive defs: clarified def (axiom name) vs. description;

eliminated obsolete thm position tags;

permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

provide actual Nitpick_HOL.extended_context;