prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

document new experimental provers

added remote iProver(-Eq) for experimentation

merged

ex/Tree23.thy: automate proof of gfull_add

ex/Tree23.thy: simplify proof of bal_del0

ex/Tree23.thy: simplify proof of bal_add0

ex/Tree23.thy: simpler definition of ordered-ness predicate

ex/Tree23.thy: prove that deletion preserves balance

more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);

more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;

tuned whitespace;

tuned signature;

tuned signature -- canonical argument order;

tuned -- Variable.declare_term is already part of Variable.auto_fixes;

ex/Tree23.thy: prove that insertion preserves tree balance and order

more IMP fragments

string -> vname

JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.

more IMP text fragments

moved latex generation for HOL-IMP out of distribution

renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)

merged

more robust, declarative and unsurprising computation of types in the quotient type definition

improve handling of bound type variables (esp. for TFF1)

improved TFF1 output

clarified signature

tuned

tuned

even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);

removed obsolete argument (cf. aa35859c8741);

removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

merged

remove unused function

also export DFG formats

always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions

added DFG unsorted support (like in the old days)

gracefully do nothing if the SPASS input file is already in DFG format

added sorted DFG output for coming version of SPASS

specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9

check "sound" flag before doing something unsound...

uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);

tuned;

more accurate class constraints on cancellation simproc patterns

tuned;

tuned Named_Thms: proper binding;

refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

slightly more explicit/syntactic modelling of morphisms;

correct import path

allow to build Probability and MV-Analysis with one ROOT.ML

removing dead code

ex/Simproc_Tests.thy: remove duplicate simprocs

use simproc_setup for cancellation simprocs, to get proper name bindings

tuned;

eliminated aliases of standard functions;

more standard attribute setup;

localized quotient data;

simplified/standardized signatures;

tuned signature;

uses IMP and hence requires its tex setup

merged

tuned text

respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

merged

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

more robust ML pretty printing (cf. b6c527c64789);

tuned;

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

tuned text

tuned names to avoid shadowing

merge Gcd/GCD and Lcm/LCM

clarify types of terms: use proper set type

instance bool :: linorder

removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

fixed typo

latex output not needed because errors manifest themselves earlier

some text on inner-syntax;

renamed in ASM

tuned order of eqns

tuned

script for exporting filtered IMP files as tar.gz

removed Norbert's email from isatest (bounces)

class Lexicon as abstract datatype;

more private stuff;

class Text.Edit as abstract datatype;

class Time as abstract datatype;

class Volatile as abstract datatype;

merged

added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file

experimental support for Scala 2.9.1.final;

class Path as abstract datatype;

class Counter as abstract datatype;

discontinued redundant ASCII syntax;

modernized specifications;

proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views); clarified Text.Range apartness, with try_restrict and try_join operations; private Perspective constructor to ensure abstract datatype integrity;

merged

tuned

merged

replacing metis proofs with facts xt1 by new proof with more readable names

more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies

disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction

NEWS

updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

removing redundant attribute code_inline in the code generator

tuned;

tuned;

improving mutabelle script again after missing some changes in f4896c792316

correcting code_prolog

merged

add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML

merged

tuned

mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties

merged

removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

removed [trans] concept from basic material

merged

tuned

merged

modernizing predicate_compile_quickcheck

adding depth as an quickcheck configuration

renamed name -> vname

removed some remaining artefacts of ancient SML code generator

NEWS

cleaner LEO-II extensionality step detection

marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs

one more LEO-II failure

merged

merged

hide typedef-generated constants Product_Type.prod and Sum_Type.sum

more uniform SZS status handling

avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"

merged

renamed B to Bc

tuned comment;

proper source positions for @{lemma};

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

tuned legacy signature;

further cleanup of stats (cf. 97e81a8aa277);

updated keywords;

really document just one code generator;

NEWS

removing old code generator

removing declaration of code_unfold to address the old code generator

removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const

removing documentation about the old code generator

removing old code generator setup for executable sets

removing old code generator setup for efficient natural numbers; cleaned typo

removing old code generator setup for real numbers; tuned

removing old code generator setup for rational numbers; tuned

removing old code generator setup for strings

removing old code generator setup for lists

removing old code generator setup for integers

removing old code generator for inductive predicates

removing quickcheck tester SML-inductive based on the old code generator

removing old code generator setup for inductive sets in the inductive set package

removing old code generator setup of inductive predicates

removing old code generator setup for product types

removing old code generator setup for function types

removing old code generator setup for datatypes

removing old code generator for recursive functions

removing old code generator setup in the HOL theory

removing invocations of the evaluation method based on the old code generator

removing invocations of the old code generator

freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing

gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations

tuned

adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra

mira: collect size of heap images

updated doc related to Satallax

parse Satallax unsat cores

merged

(old) NEWS

moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

always use sockets on Windows/Cygwin; discontinued special raw_dump facility;

mira configuration: use official polyml 5.4.1 on lxbroy10

added Term.dummy_pattern conveniences;

slightly more standard-conformant XML parsing (see also 94033767ef9b);

tuned proof

tuned type annnotation

hide not_member as also member

misc tuning and modernization;

updated to Scala 2.8.2.final;

prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;

updated to polyml-5.4.1;

updated to polyml-5.4.1;

merged

monadic bind

moved sublists to More_List.thy

NEWS

more complete stats, including small sessions which provide some clues on main HOL baseline performance;

avoid very specific code equation for card; corrected spelling

bouned transitive closure

moved acyclic predicate up in hierarchy

tuned

modernized definitions

static dummy_task (again) to avoid a few extra allocations;

tuned markup

discontinued obsolete 'types' command;

modernized structure Induct_Tacs;

tuned signature;

misc tuning and clarification;

tuned ML style;

tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;

discontinued obsolete alias structure ProofContext;

separated monotonicity reasoning and defined narrowing with while_option

include no-smlnj targets into library (cf. e54a985daa61);

increasing values_timeout to avoid SML_makeall failures on our current tests

merged

removed obsolete RC tags;

Int.thy: discontinued some legacy theorems

Set.thy: remove redundant [simp] declarations

removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++

tune text for document generation

adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well

adding code equations for cardinality and (reflexive) transitive closure on finite types

adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

adding lemma to List library for executable equation of the (refl) transitive closure

fixed typos in IMP

added nice interval syntax

Added dependecies

Added Hoare-like Abstract Interpretation

moved IMP/AbsInt stuff into subdirectory Abs_Int_Den

back to post-release mode;

Added tag Isabelle2011-1 for changeset 76fef3e57004

tuned;

updated ISABELLE_HOME_USER;

more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;

Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb

some amendments due to Jean Pichon;

correct coercion generation in case of unknown map functions

proper platform_file_url for Windows UNC paths (server shares);

proper platform_file_url;

observe base URL of rendered document; added PIDE logo;

more README;

tuned README.html;

tuned;

retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);

tuned message, which is displayed after termination of Isabelle.app on Mac OS;

keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";

tuned;

ensure Isabelle env;

Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147

tuned;

misc tuning for release;

reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;

makedist for release;

put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes

require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0

put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod

adding an example with inductive predicates to quickcheck narrowing examples

importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck

clarify platforms

killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore

updated Nitpick SAT Solver doc

update list of SAT solvers reflecting Kodkod 1.5

tuned signature;

more uniform defaults;

Quotient_Set.thy is part of library

fixed typo

standardize drive letters -- important for proper document node identification;

more user aliases;

fixed IsaMakefile action for HOL-TPTP.

prefer socket comminication on Cygwin, which is more stable here than fifos;

tuned proof;

made SML/NJ happy;

discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);

updated header;

merged;

reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)

first step towards extending Minipick with more translations

Include keywords print_coercions and print_coercion_maps

local coercion insertion algorithm to support complex coercions

printing and deleting of coercions

raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;

default print mode for Isabelle/Scala, not just Isabelle/jEdit;

augment existing print mode;

explicit option for socket vs. fifo communication;

tuned proof;

synchronized section names with manual

merged;

discontinued legacy theorem names from RealDef.thy

merged

discontinued HOLCF legacy theorem names

take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime

Moved extraction part of Higman's lemma to separate theory to allow reuse in theories compiled without support for proof terms.

Removed hcentering and vcentering options, since they are not supported by all versions of geometry.

merged

Added documentation for HOL-SPARK

drop partial monomorphic instances in Metis, like in Sledgehammer

better type reconstruction -- prevents ill-instantiations in proof replay

NEWS: mention replacement lemmas for the removed ones in Complete_Lattices

changing quickcheck_timeout to 30 seconds in mutabelle's testing

adding post-processing of terms to narrowing-based Quickcheck

HOL/ex/ROOT.ML: only list BinEx once

merged

remove redundant instantiation ereal :: power

reintroduced Minipick as Nitpick example

tuned comment

merged

Extended_Real_Limits: generalize some lemmas

add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;

made SML/NJ happy;

abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;

alternative Socket_Channel; use BinIO for fifos uniformly;

more abstract wrapping of fifos as System_Channel;

slightly more general Socket_IO as part of Pure;

more hints on Z3 configuration;

reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);

renamed inv -> filter

Added proofs about narowing

added missing makefile dependence

added example

tuned

refined comment

fixed two typos in IMP (by Jean Pichon)

merged

Updated IMP to use new induction method

New proof method "induction" that gives induction hypotheses the name IH.

official status for UN_singleton

tuned specification and lemma distribution among theories; tuned proofs

more careful treatment of initial update, similar to output panel;

proper fact binding;

syntactic improvements and tuning names in the code generator due to Florian's code review

match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test

fixed headers;

less ambiguous syntax;

tuned proofs;

merged

catch PatternMatchFail exceptions in narrowing-based quickcheck

removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition

ensuring that some constants are generated in the source code by adding calls in ensure_testable

adding abstraction layer; more precise function names

adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used

determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations

only annotating constants with sort constraints

also adding type annotations for the dynamic invocation

removed legacy lemmas in Complete_Lattices

increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling

more isatest stats;

refined Symbol.is_symbolic -- cover recoded versions as well;

double clicks switch to document node buffer;

tuned;

explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);

at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;

instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);

unique file names via serial numbers, to allow files like "root" or multiple files with same base name;

imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;

merged

numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else

removed obsolete patches for PG 4.1;

additional space for borderless UI;

more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);

explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;

isatest settings for macbroy6 (Mac OS X Lion);

more Mac OS reference hardware;

updated to SML/NJ 110.73;

tentative announcement based on current NEWS;

tuned;

separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

updated for release;

tuned;

updated generated file;

updated Complete_Lattices;

some tuning and re-ordering for release;

misc tuning for release;

more contributors;

tuned proofs;

tweak keyboard shortcuts for Mac OS X;

explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;

finite sequences as useful as introductory example;

discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;

graph traversal in topological order; Session.snapshot() with sensible defaults;

Document.Node.Name convenience;

more precise painting;

more elaborate Node_Renderer, which paints node_name.theory only;

raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;

tuned signature;

more careful traversal of theory dependencies to retain standard import order;

sane default for class Thy_Load;

removed obsolete patches for PG 4.1;

specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;

added "isabelle scalac" convenience;

Symbol.explode as in ML;

ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;

dropped unused argument – avoids problem with SML/NJ

tuned spacing

tuned

tuned post fixpoint setup

merged

when applying induction rules, remove names of assumptions that come with the rule in case the rule is transformed by the simplifier due to instantiations

remove stray "using [[simp_trace]]"

tune indenting

removed unused legacy lemma names, some comment cleanup.

removed word_neq_0_conv from simpset, it's almost never wanted.

removed further legacy rules from Complete_Lattices

NEWS on Complete_Lattices, Lattices

tail recursive proof preprocessing (needed for huge proofs)

tuning

merged

revised AbsInt and added widening and narrowing

updated comment

updated generated code

tuned

renamed Complete_Lattices lemmas, removed legacy names

merged

create central list for language extensions used by the haskell code generator

observe distinction between sets and predicates

merged

cleand up AbsInt fixpoint iteration; tuned syntax

tuned proofs

tuned proofs

remove some redundant [simp] declarations; simplify some proofs;

tune proofs

tune simpset for Complete_Lattices

merged

added lemma motivated by a more specific lemma in the AFP-KBPs theories

simplified unsound proof detection by removing impossible case

correcting NEWS

correcting theory name and dependencies

renamed AList_Impl to AList

fastsimp -> fastforce in doc

fix typo

shorten proof of frontier_straddle

NEWS and CONTRIBUTORS

remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def

simplify proofs using LIMSEQ lemmas

remove trivial lemma Lim_at_iff_LIM

fix typos

NEWS for euclidean_space class

move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

adding NEWS and CONTRIBUTORS

merged

correcting imports after splitting and renaming AssocList

tuned

moving connection of association lists to Mappings into a separate theory

adding NEWS and CONTRIBUTORS

tuned some symbol that probably went there by some strange encoding issue

added my contributions to NEWS and CONTRIBUTORS

fixed type intersection (again)

consistent option naming

NEWS fastsimp -> fastforce

new fastforce replacing fastsimp - less confusing name

merged

NEWS for Library/Product_Lattice.thy

misc tuning and clarification;

merged

merged

tuned proofs

Library/Saturated.thy: 'Sat' abbreviates 'of_nat'

more CONTRIBUTORS;

persistent ISABELLE_INTERFACE_CHOICE;

explicit choice of interface;

more orthogonal signature;

updates for release;

misc tuning and clarification (NB: settings are already local for named snapshots/releases);

some updates of PLATFORMS;

more README;

merged

mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)

misc tuning;

misc tuning and clarification;

speed up slow proof;

merged

more modularization

stronger colors (as background);

some color scheme for theory status;

some keyboard shortcuts for important actions; proper label properties, which are also required for jEdit "Shortcuts" options panel;

explicit jEdit actions -- to enable key mappings, for example;

more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;

tuned usage;

simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);