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