tuned;

added Promise.fulfill_result;

slightly shorter tail (again) -- theory loader produces less warning spam (cf. 2524c1bbd087);

kill failed theories in reverse order -- avoids cascaded warnings;

discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);

Standard_System.raw_exec; more robust root.mkdirs;

removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;

added Cygwin "make" package;

discontinued old ISABELLE and ISATOOL environment settings;

shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;

removed further remains of mutable theory data (cf. 25bd3ed2ac9f);

merged

code cache only persists on equal theories

moved name duplicates to end of theory; reduced warning noise

merged

modernized

added applify combinator

dropped redundant name declarations

dropped copy operation for legacy TheoryDataFun

code cache without copy; tuned

report keywords as singleton messages, control message kind via print mode;

explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);

omit useless (?) scaladoc;

added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;

after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;

discontinued special HOL_USEDIR_OPTIONS;

updated stats;

made SML/NJ happy;

merged

removed legacy asm_lr_simp_tac

removed more asm_rl's - unfortunately slowdown of 1 min.

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

simplified

absorb structures Decompose and Descent into Termination, to simplify further restructuring

another legacy "asm_lr"

merged

removed legacy asm_lr

merged

added lemmas

added lemma

removed FIXME

tuned error handling;

Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;

Download URLs -- with progress monitor.

Future values -- Scala version.

added simple dialogs;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System; tuned;

eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;

tuned signature;

less ambitious isatest for SML/NJ;

killed a few warnings

more regular axiom of infinity, with no (indirect) reference to overloaded constants

back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;

explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;

tuned;

crude Cygwin.setup;

ignore undefined environment;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned;

system shutdown hook: strict kill;

moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);

pid without newline -- required for Scala version of system_out;

higher-order treatment of temporary files;

isabelle_tool: apply platform_path only once; tuned;

slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");

some sanity checks for symbol interpretation;

allow UTF-8 in theory and file names;

factored-out Library.decode_permissive_utf8;

read header by scanning/parsing file;

quoted_content: handle escapes;

scan: operate on file (via Scan.byte_reader), more robust exception handling;

added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

removed unused read_file;

tidied proofs

made sml/nj happy

updated certificates

updated example

merged verification condition structure and term representation in one datatype, extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths), simplified discharging of verification conditions (due to improved datatype), added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

merged

updated generated document sources

take care for destructive print mode properly using dedicated pretty builders

merged

made sml/nj happy

merged

dropped junk

reduced code generator cache to the baremost minimum

updated documentation

updated generated examples

reduced code generator cache to the baremost minimum; corrected spelling

basic setup for header scanning/parsing;

clarified atom parser: return content; added tags parser;

tuned;

renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);

Isabelle session manager -- most basic setup;

actually closer file reader;

tuned;

added plain read_file;

consider proper input only; added wrappers;

added completion -- lazy avoids excessive table building; tuned signature;

Generic parsers for Isabelle/Isar outer syntax -- Scala version.

class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure; added Token_Reader; tuned;

Changes in generated code, apparently caused by changes to the code generation system itself.

Polishing up the English

merged

merged

clarified various user-defined syntax issues

prefer prefix "iso" over potentially misleading "is"; tuned

moved lemmas o_eq_dest, o_eq_elim here

add 'morphisms' option to domain_isomorphism command

merged

generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs

rename equals_zero_I to minus_unique (keep old name too)

add lemma swap_triple

improve performance by reordering of parser combinators;

added nested comments; tuned;

more Scala sources;

simiplified result of keyword parser (again); sort completions by plain string order; moved Reverse to library.scala;

simplified result of keyword and symbols parser; some support for parsing outer syntax tokens;

Outer lexical syntax for Isabelle/Isar -- Scala version.

refined some Symbol operations/signatures; tuned;

refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;

added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;

indicate final state of keywords; added symbol scanner;

added symbol classification; tuned;

tuned;

merged

imitate PG style;

merged

imitate PG colors;

made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default; up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option

merged

polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation

merged

added support for binary nat/int representation to Nitpick

distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick; this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on

merged

get rid of polymorphic equality in Nitpick's code + a few minor cleanups

added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections

markup bad YXML as malformed; removed unused XML.document; removed unused markup;

replace invalid code points -- instead of exception;

tuned signature;

removed junk (cf. f49d45afa634);

merged

merged

add lemma INFM_conjI

added lemmas about INFM/MOST

add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff

add lemmas open_image_fst, open_image_snd

Result.cache;

cache for partial sharing;

merged

Two new theorems about cardinality

replace 'UNIV - S' with '- S'

re-state lemmas using 'range'

make proof use only abstract properties of eventually

swap_self already declared [simp]

declare swap_self [simp], add lemma comp_swap

fifo: raw byte stream; Result: fully decoded symbols and tree structure; adapted to simplified message format; tuned;

added decode_chars, with raw character view on byte buffer and adhoc decoding via toString; parse/chunks: avoid direct string comparison, to make it actually work with abstract CharSequence;

tuned signature;

tuned;

simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;

robust representation of low ASCII control characters within XML/YXML text;

merged

filter out identical completions;

spaces not allowed, unfortunately

user aliasses

merged

replaced blast by metis (blast hangs with polyml-5.2)

avoid negative indices as argument ot drop

Upgraded a warning to an error

merged

improved crude deriving_show inference

explicit name for function space

make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits

make Nitpick "Core" test more conservative, to avoid problems on Larry's machine

made sml/nj happy

also sort verification conditions before printing

print assertions in a more natural order

removed unique ids -- now in session.scala;

merged

Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;

Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;

merged

repaired accident: do not forget module contents if there are no imports

option width for Code_Target.code_of

default_code_width is now proper theory data

merged

updated dependencies

make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations

depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)

merged

moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

avoid dependency on implicit dest rule predicate1D in proofs

merged

NEWS

merged

merged

take and drop as projections of chop

explicit lower bound for index

merged

merged

streamlined proofs

fixed typo

merged

only invoke metisFT if metis failed

added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas

merged

each import resides in its own line

using existing lattice classes

added get_data;

sealed XML.Tree; keep original XML.Tree within DOM as user data;

simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway);

slightly more robust and less ambitious version of install_fonts;

more robust Cygwin.config: actually check Wow6432Node, prefer explicit CYGWIN_ROOT in any case;

merged

merged

merged

made Nitpick work also for people who import "Plain" instead of "Main"

make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes

keep future Isabelle application entry point;

merged

also consider the fully-typed version of metis for Mirabelle measurements

merged

made SML/NJ happy

simplified notion of empty module name

commit

resorted code equations from "old" number theory version

merged

split off evaluation mechanisms in separte module Code_Eval

register_fonts: more precise error handling;

added future;

depend on Java 1.6 after all;

basic support for IsabelleText fonts;

merged

merged

tuned inner structure

merged Crude_Executable_Set into Executable_Set

merged

avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy"); this produces two copies of the same module, with separate references etc.

better error message in Refute when specifying a non-existing SAT solver

merged

updated certificate

merged

repaired read_const_expr, broken in 1e7ca47c6c3d

merged

verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization), custom-made (top-down) atomize_conv, store predicate and function symbols in a table instead of a list for faster lookup, updated certificates

merged

tuned proofs

tuned lattices theory fragements; generlized some lemmas from sets to lattices

avoid lazy val with side-effects -- spurious null pointers!?

toString: more robust handling of null; tuned;

proper markup text for loc;

output_syms: permissive treatment of control symbols, cf. Scala version;

basic treatment of special control symbols; misc tuning;

elements: more convenient result;

more robust treatment of line breaks -- Java "split" has off semantics;

added auxiliary constructors;

added elements: Interator; first isHighSurrogate, not isLowSurrogate; misc tuning and generalization;

merged

merged

tuned whitespace

merged, resolving minor conflicts

NEWS

signatures for generated code; tuned

tuned

avoid misleading name "superarities"

more speaking function names for Code_Printer; added doublesemicolon

tuned code setup

version of IsabelleMono that retains plain ASCII and ISO-LATIN-1 from Bitstream Vera;

output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4; output_width: uniform mapping -- avoid obscure fastpath optimization;

added markup for hidden text; handle "\<^bold>" as markup; HTML output: include original control symbols as hidden text, to enable copy-paste;

Basic HTML output.

output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);

fixed paths in Nitpick's ML file headers

added soundness fix to Nitpick's history

export symbols from Minipick (so I can use them in other programs)

make proof work again

fix soundness bug in Nitpick's "destroy_constrs" optimization

merged, resolving minor conflict, and recovering sane state;

merged

merged

merged, resolving minor conflicts;

merged

merged

modernized structure Datatype_Aux

tuned

dropped some unused bindings

modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML

more accurate linerarity

merged

Inl and Inr now with authentic syntax

renamed former datatype.ML to datatype_data.ML

renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML

modernized; dropped ancient constant Part

centralized sum type matter in Sum_Type.thy

tuned

bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)

merged

normalized uncurry take/drop

merged

curried take/drop

backported parts of abstract byte code verifier from AFP/Jinja

added document_node; tuned comments;

document init_component shell function;

back to after-release mode;

back to main repository;

merged

merged

added Crude_Executable_Set

removed redundant lemma

added remdups_filter lemma

merged

subst_signatures

tuned

exported build_tsig

crude support for type aliasses and corresponding constant signatures

generalized some lemmas

added Crude_Executable_Set.thy

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