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;

tuned;

tuned thread data;

worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock); worker_start: back to non-self version; scheduler: status output based on ticks;

slightly leaner and more direct control of worker activity etc.;

adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example

adapted the inlining in the predicate compiler

recursively replacing abstractions by new definitions in the predicate compiler

merge

add fixrec support for HOL pair constructor patterns

define cprod_fun using Pair instead of cpair

add (LAM (x, y). t) syntax and lemma csplit_Pair

lexicographic order: run local descent proofs in parallel

merged

domain package no longer uses cfst/csnd/cpair

conceal partial rules depending on config flag (i.e. when called via "fun")

conceal "termination" rule, used only by special tools

do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional

modernized structure XML_Syntax;

structure Thm_Deps;

modernized structure Proof_Node;

modernized structure Proof_Display;

modernized structure Proof_Syntax;

modernized structure Local_Syntax;

modernized structure AutoBind;

modernized structure Primitive_Defs;

modernized structure Simple_Syntax;

modernized structure Context_Position;

observe usual naming conventions;

find_theorems: respect conceal flag

DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);

back to warning -- Proof General tends to "popup" tracing output;

split parsing of counterexamples from translation into terms (avoids Term.dummyT and ill-typed terms)

merged

predicate compiler creates code equations for predicates with full mode

renamed rpred to random

Rules that characterize functional/relational specifications.

adapted Item_Net; tuned;

allow multi-index; more scalable merge; renamed delete to remove, and insert to update (standard naming conventions); tuned;

added insert_safe, delete_safe variants;

tuned signature;

modernized structure Context_Rules;

modernized structure Rule_Cases;

merged

dedicated theory for loading numeral simprocs

set Pure theory name properly

tuned code setup

some notes on SPASS 3.0 distribution;

merged

combined former theories Divides and IntDiv to one theory Divides

tuned variable names of bindings; conceal predicate constants

dedicated theory for loading numeral simprocs

moved some div/mod lemmas to theory Divides

tuned proof

moved Commutative_Ring into session Decision_Procs

abstract over variables in reversed order (application uses given order)

disable printing of unparsed counterexamples for CVC3 and Yices

pattern are separated only by spaces (no comma)

back to polyml-svn -- performance impact is minimal, slowdown was caused by accumulated cruft of long-running Mac OS;

less verbose termination tactics

less verbose inductive invocation

tuned

absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned

merged

recovered from 7a1f597f454e, simplified imports;

merged

merged

adjusted to changes in theory Divides

moved some lemmas to theory Int

moved some dvd [int] facts to Int

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

eliminated some old folds;

eliminated some old folds;

eliminated some old folds;

less aggressive tracing;

DEEPEN: less aggressive tracing, subject to trace_DEEPEN;

merged

merged

removing ancient predicate compiler files

merged

encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy

improved mode parser; added mode annotations to examples

moved datatype mode and string functions to the auxillary structure

improving mode parsing in the predicate compiler

improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler

merged

Tidied up some very ugly proofs

small fixes

merged

join entries properly on theory merge

moved some dvd [int] facts to Int

moved algebraic classes to Ring_and_Field

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

standardized filter/filter_out;

modernized some structure names;

eliminated obsolete/unused Thm.kind_internal/is_internal etc.;

modernized functor/structures Interpretation;

tuned whitespace;

unregister: eliminated unused status;

proper header;

proper header; tuned whitespace;

proper header; adapted ResBlacklist -- eliminated inefficient hash table; eliminated some old folds;

separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

Named_Thms is not scalable;

replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space; tuned;

tuned;

tuned proof;

separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;

removed unused file;

less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;

removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping; (NB: in principle symbol abbreviations could well be ambigous);

simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output

merged

adjusted import to changed HOL theory graph

moved theory Divides after theory Nat_Numeral; tuned some proof texts

proper nested quotes; give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);

components: ensure that the last line is read, even if it lacks EOL;

updated Isar.goal;

renamed raw Proof.get_goal to Proof.raw_goal;

back to Proof.raw_goal;

renamed Proof.flat_goal to Proof.simple_goal;

Isar.goal: Proof.simple_goal, not raw version;

replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;

provide SpecParse.constdecl/constdef, e.g. for quotient_definition;

slightly more robust error message;

tuned;

merged

merged

misc tuning;

let naming transform binding beforehand -- covering only the "conceal" flag for now; export LocalTheory.standard_morphism;

tuned;

simplified default binding; conceal internal bindings;

conceal internal bindings;

Drule.store: proper binding; conceal internal bindings;

added restore_naming;

load Product_Type before Nat; dropped junk

moved lemmas for dvd on nat to theories Nat and Power

Probability tweaks

merged

New theory Probability, which contains a development of measure theory

merged

New theory SupInf of the supremum and infimum operators for sets of reals.

eliminated hard tabulators, guessing at each author's individual tab-width;

tuned initial session setup;

merged

proper headers;

reactivated sun-poly, as parallel test;

merged

merged

merged

merged

merged

disabled test case for predicate compiler due to an problem in the inductive package

added examples for quickcheck prototype

adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex

adding test case for inlining of predicate compiler

hiding randompred definitions

changes to example file

print retrieved specification when printing intermediate results

added option show_modes to predicate compiler

including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck

removed unused file smt_builtin.ML, made negative pattern polymorphic (similar to positve pattern)

included description for sledgehammer options in Mirabelle script

measure runtime of ATPs only if requested

eliminated some old folds;

eliminated some old folds;

Datatype.read_typ: standard argument order; eliminated some old folds;

normalized basic type abbreviations;

misc tuning and simplification;

merged

merged

merged

merged

tuned

tuned

dropped obsolete comment

added implode and explode

added friendly error message when Kodkodi is not available

internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi

merged

merged

made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers

more thread-safe access to global refs;

avoid structure alias;

comment;

non-critical output -- ship message in one piece;

ProofContext.setmp_verbose_CRITICAL;

non-critical atomic accesses;

critical comments;

tuned;

SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;

max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;

lemma converse_inv_image

authentic constants; moved "acyclic" further down

point-free characterization of well-foundedness

replaced (outdated) comments by explicit statements

reactivated test on sunbroy2 -- with full proof parallelism (requires Poly/ML-SVN-921);

forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;

tuned;

added nitpick manual here;

recovered sort indentation for "sort position", as documented in the file; more precise dependencies -- HOL-Multivariate_Analysis produces an image; tuned;

tuned white space;

merged

merged

avoid upto if not needed

conceal quickcheck generators

merged

merged

make Nitpick compile again

merged

be somewhat more liberal in Nitpick about which types may occur in formulas

make the Nitpick examples work again

updated keyword files to include "nitpick" and "nitpick_params"

continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.

updated Nitpick documentation to remove weird default for "overlord"

updated Nitpick manual to reflect the latest Stand der Dinge

merged

wrap line correctly in Nitpick documentation

added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.

Added Nitpick manual.

merged

Added Pattern.thy to Nominal/Examples.

merged

tuned

added SML_Quickcheck import

tuned code setup for primitive boolean connectors

legacy warnings for old-style term styles

removed unnecessary NameSpace prefix;

misc tuning and updates;

merged

implicit default is 4 cores -- more cost-effective;

deleted junk;

more precise dependencies, notably for HOL-Multivariate_Analysis;

re-moved theory Fin_Fun to AFP

merged

distinguished session for multivariate analysis

adjusted to changes in corresponding ML code

eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;

maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;

name space groups are identified by serial, not serial_string;

maintain group via name space, not tags; tuned;

LocalTheory.naming_of;

begin_theory: set theory_name here;

maintain group via name space, not tags;

maintain proper Name_Space.naming, with conceal and set_group; maintain group via name space, not tags; tuned signature; tuned;

more direct access to naming; tuned signature;

Name_Space.naming: maintain group and theory_name as well; tuned;

export is_concealed; tuned;

merge_list: no exception DUP here;

merged

more uniform ISABELLE_USEDIR_OPTIONS;

make SML/NJ happy;

conceal consts via name space, not tags;

allow name space entries to be "concealed" -- via binding/naming/local_theory;

switch to polyml-5.2.1 to see if it impacts performance;

merged

Multivariate polynomials library over fields

A theory of polynomials based on lists

Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)

merged

further changes due to the previous merge in the predicate compiler

merge -- imported from bulwahn d759e2728188;

removed tuple functions from the predicate compiler

improving the compilation with higher-order arguments in the predicate compiler

now the predicate compilere handles the predicate without introduction rules better as before

removed dead code; added examples

removed obsolete GeneratorPrem; clean-up after modularization; tuned

modularized the compilation in the predicate compiler

adapted parser for options in the predicate compiler

modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples

cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names

added skip_proof option; playing with compilation of depth-limited predicates

reinvestigating the compilation of the random computation in the predicate compiler

added option to generate random values to values command in the predicate compiler

commented out the random generator compilation in the example file

added option to execute depth-limited computations for the values command in the predicate compiler

renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler

simplified and improved compilation of depth-limited search in the predicate compiler

moved argument expected_modes into options; improved mode check to only check mode of the named predicate

removed unnecessary argument rpred in code_pred function

added option show_mode_inference; added splitting of conjunctions in expand_tuples

changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned

further cleaning up

added option show_proof_trace

importing of polymorphic introduction rules with different schematic variable names

added option show_intermediate_results

continued cleaning up; moved tuple expanding to core

cleaned up debugging messages; added options to code_pred command

added first support for higher-order function translation

added to process higher-order arguments by adding new constants

cleaned up

added theory with alternative definitions for the predicate compiler; cleaned up examples

importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first

higher-order arguments in different rules are fixed to one name in the predicate compiler

changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned

changed proof method to handle widen predicate in JinjaThreads

added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex

processing of tuples in introduction rules

added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions

developing an executable the operator

generalizing singleton with a default value

changed elimination preprocessing due to an error with a JinjaThread predicate

added test for higher-order function inductification; added debug messages

added filtering of case constants in the definition retrieval of the predicate compiler

extended core of predicate compiler to expand tuples in introduction rules

added tupled versions of examples for the predicate compiler

moved meta_fun_cong lemma into ML-file; tuned

merged

adapted Function_Lib (cf. b8cdd3d73022);

configuration flag "partials"

renamed auto_term.ML -> relation.ML

function package: more standard names for structures and files

renamed FundefDatatype -> Function_Fun

maintain position of formal entities via name space;

maintain explicit name space kind; export Name_Space.the_entry; tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; simplified messages;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

maintain abstract entry, with position, identity etc.; declare/define: explicit indication of strictness; merge_tables/join_tables: disallow duplicates based on entry identity;

tuned message;

import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);

markup for formal entities, with "def" or "ref" occurrences;

handle Sorts.CLASS_ERROR instead of arbitrary exceptions;

reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;

merged

turned off old quickcheck

pat_completeness gets its own file

ignore error messages produced by ATPs

merged

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)

restored accidentally deleted submultiset

multiset operations with canonical argument order

arg_types_of auxiliary function; using multiset operations

merged

close thm derivations explicitly

Fix a duplicate abbreviation || in etc/symbols.

made SML/NJ happy;

updated session name;

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);

merged

merged

merged

use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);

merged

explicit close_derivation

merged

map_range (and map_index) combinator

dropped Datatype.distinct_simproc

use Synchronized.assign to achieve actual immutable results;

support single-assigment variables -- based on magic RTS operations by David Matthews;

merged

fixed permissions -- this is a script, not an executable

inv_onto -> inv_into

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

merged

fixed the "expect" mechanism of Refute in the face of timeouts

removed "nitpick_const_simp" attribute from Record's "simps"; Nitpick has its own notion of a record and doesn't need those.

merged

more accurate removal

merged

curried inter as canonical list operation (beware of argument order)

merged

proper handling of single literal case, added explicit exception, unfolding of distinct respects equal elements, made SML/NJ happy

Removed the hard-wired white list of theorems for sledgehammer

merged

Some new lemmas concerning sets

merged

curried union as canonical list operation

tuned ML import

removed old-style \ and \\ infixes

merged

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

find_theorems: better handling of abbreviations (by Timothy Bourke)

standardized basic operations on type option;

eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;

tuned;

fixed SML/NJ toplevel pp; tuned;

backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;

tuned;

uniform use of Integer.min/max;

modernized session SET_Protocol;

modernized session Metis_Examples;

modernized session Isar_Examples;

tuned header;

more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;

removed unused map_force;

Removal of the unused atpset concept, the atp attribute and some related code.

additional schematic rules for Z3's rewrite rule

merged

added Hilbert_Choice section

merged

eliminated extraneous wrapping of public records, replaced simp_tac by best_tac (simplifier failed), less strict condition for rewrite (can also handle equations with single literal on left-hand side)

proper exceptions instead of unhandled partiality

footnote: inv via inv_onto

added inv_def for compatibility as a lemma

slightly less context-sensitive settings;

merged

corrected paths to certificates, added note how to re-generate the certificates

added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)

merged

merged

more accurate checkpoints

dropped lazy code equations

CONTRIBUTORS

always qualify NJ's old List.foldl/foldr in Isabelle/ML;

eliminated duplicate fold1 -- beware of argument order!

uniform use of Integer.add/mult/sum/prod;

Removed dead code in function mk_deftab.

Removed unneeded reference to inv_def.

Replaced inv by the_inv_onto.

Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).

fixed proof (cf. d1d4d7a08a66);

removed disjunctive group cancellation -- provers run independently; sledgehammer: kill earlier session, and removed obsolete max_atps; tuned;

tuned;

removed some unreferenced material; tuned;

merged

certificates for sos

merged

added sums of squares for standard deviation

merged

Inv -> inv_onto, inv abbr. inv_onto UNIV.

disable indent-tabs-mode in Proof General / Emacs;

merged

made SML/NJ happy;

Merged.

Finished revisions of locales tutorial.

Changed part of the examples to int.

Save current state of locales tutorial.

Observe order of declaration when printing registrations.

disable sunbroy2 for now;

tuned/moved divide_and_conquer';

tuned;

removed separate record_quick_and_dirty_sensitive;

simplified tactics; use proper SUBGOAL/CSUBGOAL;

eliminated old List.foldr and OldTerm operations; misc tuning;

removed unused names;

misc tuning and simplification;

less pervasive names;

operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;

Method.cheating: check quick_and_dirty here;

tuned;

Unsynchronized.set etc.;

indicate CRITICAL nature of various setmp combinators;

ISABELLE_TOOL;

tuned signature; observe coding conventions of this file;

merged

merged

added the_inv_onto

eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;

removed obsolete old goal command;

legacy Drule.standard is no longer pervasive;

explicitly qualify Drule.standard;

tuned white space;

local channels for tracing/debugging;

made SML/NJ happy;

sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;

replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;

space_implode;

normalized aliases of Output operations;

eliminated slightly odd get/set operations in favour of Unsynchronized.ref; eliminated aliases of Output operations; print_cert: use warning for increased chance that the user actually sees the output; misc tuning and simplification;

natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system;

ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification;

tuned proof (via atp_minimized);

sort_strings (cf. Pure/library.ML);

clarified File.platform_path vs. File.shell_path; tuned;

exported File.shell_quote;

misc tuning and recovery of Isabelle coding style;

eliminated extraneous wrapping of public records; tuned;

tuned signature; tuned;

renamed functor HeapFun to Heap;

misc tuning and clarification;

structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

modernized structure names;

show direct GC time (which is included in CPU time);

eliminated obsolete C/flip combinator;

added List.nth

tuned make parameters for sunbroy2;

accomodate old version of "tail", e.g. on sunbroy2;

settings for parallel experimental Poly/ML 5.3;

sharpened name

more explicit notion of canonized code equations

more explicit notion of canonized code equations