updated to official Poly/ML 5.3.0;

switched some isatest sessions to official Poly/ML 5.3.0;

setup for official Poly/ML 5.3.0, which is now the default;

locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;

eliminated hard tabulators;

fixed some inappropriate names

merged

New theory Probability/Borel.thy, and some associated lemmas

merged

tuned error messages; tuned code

follow standard theory merge behaviour: do not change already selected solver

generalized proof by abstraction, abstract propositional nnf goals (lets best_tac succeed on very large terms)

made theory merge deterministic wrt. the selected solver

merged

merged

Repaired handling of comprehensions in "values" command.

updated functor Theory_Data, Proof_Data, Generic_Data;

modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;

adapted Theory_Data; tuned;

adapted Theory_Data; handle Symtab.DUP during actual merge;

tuned;

adapted Generic_Data, Proof_Data; tuned;

adapted Generic_Data; proper merge of fst/fst and snd/snd;

modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;

added "declaration (pervasive)";

print_theorems: suppress concealed (global) facts, unless "!" option is given;

updated generated file;

modernized structure Random_Word;

init_component: slightly more robust read (raw input, succeed on non-terminated last line);

merged

Due to popular demand: added a function that benchmarks proof reconstruction for a single DIMACS CNF file.

Turned sections into subsections (better document structure).

merged

merged

fix name of lemma snd_strict

use try instead of handle

map functions for various types, with ep_pair/deflation/finite_deflation lemmas

lemma deflation_strict

tuned ML_OPTIONS for SML/NJ -- for improved performance;

merged

added predicate example

tuned

modernized primrec

made SML/NJ happy

merged

merged

Replaced exception CRing by error because it is meant for the user.

merged

Command atp_minimize uses the naive linear algorithm now because the binary chop one had turned out to be a little bit suboptimal. Internally the binary chop one is still available.

merged

merged

merged

merge

merged

adopted the predicate compile quickcheck

made definition of functions generically for the different instances

renamed generator to random_function in the predicate compiler

improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered

strictly respecting the line margin in the predicate compiler core

adopted mode syntax for values command

disabled upt example because of a problem due to overloaded constants with the predicate compiler

added optional mode annotations for parameters in the values command

moved values command from core to predicate compile

added further example of the values command

Adopted output of values command

improved handling of overloaded constants; examples with numerals

made SML/NJ happy; tuned

adding tracing function for evaluated code; annotated compilation in the predicate compiler

added documentation for local SMT solver setup and available SMT options, added verbose output for SMT solver invocation, test if local SMT solver exists before invoking it, always trace (possible) counterexamples, documented existence of SMT server

renamed method induct_scheme to induction_schema

NEWS

removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)

renamed method sizechange to size_change

added boehmes and hoelzl to isatest mailings

merged

tuned

Merged.

Merged.

Use PrintMode.setmp to make thread-safe; avoid code clones.

Make output indenpendent of current print mode.

Relax on type agreement with original context when applying term syntax.

tuned;

proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context; tuned signature; tuned;

adapted LocalTheory.declaration;

allow "pervasive" local theory declarations, which are applied the background theory;

declare Spec_Rules for most basic definitional packages;

misc tuning and clarification;

scalable version of Named_Thms, using Item_Net;

merged

merged

more accurate cleanup;

merged

more accurate dependencies;

merged

handle let expressions inside terms by unfolding (instead of raising an exception), added examples to test this feature

shorter names for variables and verification conditions, auto-fix variables occurring in a verification condition

added references to HOL-Boogie papers

tuned header; use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;

made SML/NJ happy; normalized type abbreviations;

eliminated funny record patterns and made SML/NJ happy;

proper header; eliminated SML97's opaque signature constrain, which is essentially a legacy feature (due to problems with ML toplevel pretty printing);

more accurate dependencies; tuned;

merged

added Tree23 to IsaMakefile

New

merged

fixed order of parameters in induction rules

added bulwahn to isatest mailings

merged

Completely overhauled

better error handling for fixrec_simp

add more fixrec_simp rules

fixrec examples use fixrec_simp instead of fixpat

domain package registers fixrec_simp lemmas

merged

add fixrec_simp attribute and method (eventually to replace fixpat)

proper and unique case names for the split_vc method, shortened label names, added an example demonstrating the split_vc method

merged

merged

always be qualified -- suspected smartness in fact never worked as expected