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