added a tabled implementation of the reflexive transitive closure

merged

merged

improved ML interface to pcpodef

use Drule.standard (following typedef package), add pcpodef tactic interface

eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";

eliminated obsolete "internal" kind -- collapsed to unspecific "";

unused_thms: ignore kind -- already observes "concealed" flag;

all_valid_thms: more sophisticated check against global + local name space;

Remove map_compose, replaced by map_map

New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key

Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute

merged

accomplish mutual recursion between fun and inst

moved lemma map_of_zip_map to Map.thy

merged

explicit code lemmas produce nices code

repaired broken code_const for term_of [String.literal]

fixed soundness bug in Nitpick related to sets

removed unnecessary oracle in the predicate compiler

improving code quality thanks to Florian's code review

renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name

announcing the predicate compiler in NEWS and CONTRIBUTORS

new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler

removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming

added another example to the predicate compiler * * * tuning examples

changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned

removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main

adopted predicate compiler examples to new syntax for modes

added interface of user proposals for names of generated constants

first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes

adding more tests for the values command; adding some forbidden constants to inductify * * * added further testcase for values command

Enables tests for locale functionality that is now available.

merged

uniform use of simultabeous use_thys;

merged

explicit invocation of code generation

adding code equations for constructors

tuned

changed URL of SMT server, added Z3 rewrite lemma

Added two new lemmas

tuned imports

tuned

local mutex for theory content/identity operations;

admit dummy implementation;

Toplevel.thread provides Isar-style exception output;

generalized Runtime.toplevel_error wrt. output function;

exported SimpleThread.attributes;

plain add_preference, no setmp_CRITICAL required;

adapted Theory_Data;

recovered update from 7264824baf66, which got lost in 7264824baf66;

merged

merged

tuned header

substantial simplification restores code generation

lemmas about apfst and apsnd

tuned imports

merged

HOLCF example: domain package proofs done manually

add lemma parallel_fix_ind

add title/author block

theory of representable cpos

add map_map lemmas

add in_deflation relation, more lemmas about cast

ep_pair and deflation lemmas for powerdomain map functions

remove spurious parameter to "merge"

merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)

fixed soundness bug in Nitpick related to sets of sets; (detected thanks to the TPTP)

added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype

added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes

don't promise too much in the Nitpick manual

merged

added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package; this ensures that Nitpick can find the definition and determine whether its inductive or coinductive

merged

try very hard to remove temporary files generated by Nitpick in case of interruption

eliminate two FIXMEs in Nitpick's monotonicity check code

rename "NitpickMono" to "Nitpick_Mono" in example

merged

minor cleanup in Nitpick

make "auto" SAT solver less verbose

make "sizechange_tac" slightly less verbose

don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)

readded Predicate_Compile to Main

merged

fixed error in Nitpick's display of uncurried constants, which resulted in an exception

fixed minor problems with Nitpick's documentation

merged

merged my Auto Nitpick change with Lukas's Predicate Compiler changes

introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian

use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation

fix typo in Nitpick manual

optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem

clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak

renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary

eliminated some old uses of cumulative prems (!) in proof methods;

eliminated some unused/obsolete Args.bang_facts;

modernized structure Theory_Target;

removed unused Quickcheck_RecFun_Simps;

define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

bang_facts: legacy feature;

tuned proofs;

removed obsolete name_of -- cf. decode;

desymbolize: use Symbol.decode directly; recovered coding conventions of this file;

try SAT_Examples last, to minimize impact of global side-effects;

home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);

Inserted missing theory dependency

merged

Merged.

Removed obsolete code.

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

pretty name for ==>

added HOL-Boogie

added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception), replaced unspecific 'error' invocations with raising of specific SMT exceptions, added annotations to traced SMT problem and solver output

ignore parsing errors, return empty assignment instead

scheduler: clarified interrupt attributes and handling;

worker_next: plain signalling via work_available only, not scheduler_event; scheduler: tuned worker pool adjustments;

revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

avoid broadcast work_available, use daisy-chained signal instead; max_threads: allow as much as 4 * m, after extra delay;

fulfill_proof_future: tuned important special case of singleton promise;

worker_next: treat wait for work_available as Sleeping, not Waiting; max_threads: simple adaptive scheme between m and 2 * m;

worker activity: distinguish between waiting (formerly active) and sleeping; tuned;