merged

fix monotonicity type of None

compile

introduced hack to exploit the symmetry of equality in monotonicity calculus

cleanup example

add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule

fixed bug in monotonicity solution display, whereby the polarity of literals was ignored

improve precision of forall in constancy part of the monotonicity calculus

added some missing well-annotatedness constraints to monotonicity calculus

more work on the monotonicity evaluation driver

improve precision of finite functions in monotonicity calculus

added ML code for testing entire theories for monotonicity

use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus

added examples to exercise new monotonicity code

fixed quantifier handling of new monotonicity calculus

tune parentheses and indentation

proper handling of frames for connectives in monotonicity calculus

tune indentation

removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications

implemented All rules from new monotonicity calculus

fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints

started implementing the new monotonicity rules for application

implemented connectives in new monotonicity calculus

added "Neq" operator to monotonicity inference module

started implementing connectives in new monotonicity calculus

more work on frames in the new monotonicity calculus

support 3 monotonicity calculi in one and fix soundness bug

tuning

proper handling of assignment disjunctions vs. conjunctions

adapt monotonicity code to four annotation types

more monotonicity tuning

tuning

added frame component to Gamma in monotonicity calculus

use boolean pair to encode annotation, which may now take four values

started generalizing monotonicity code to accommodate new calculus

merged

handle "max_relevant" uniformly

honor the default max relevant facts setting from the SMT solvers in Sledgehammer

have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?

return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction

trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

reraise interrupt exceptions

[mq]: sledge_binary_minimizer

correcting usage documentation in mirabelle tool

adding mutabelle as a component and an isabelle tool to be used in regression testing

commenting out sledgehammer_mtd in Mutabelle

removing declaration in quickcheck to really enable exhaustive testing

adding timeout to try invocation in mutabelle

adding filtering, sytactic welltyping, and sledgehammer method in mutabelle

replace `type_mapper` by the more adequate `type_lifting`

moved bootstrap of type_lifting to Fun

replace `type_mapper` by the more adequate `type_lifting`

avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;

IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;

command 'notepad' replaces former 'example_proof';

prefer 'notepad' over 'example_proof';

merged

more intimate definition of fold_list / fold_once in terms of fold

canonical fold signature

formal notepad without any result;

added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;

eliminated obsolete Token.Malformed -- subsumed by Token.Error;

tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);

added Syntax.pretty_priority;

merged

conventional point-free characterization of rsp_fold

replaced memb by existing List.member

explicit type constraint; streamlined notation

tuned proposition

lemma multiset_of_rev

lemmas fold_remove1_split and fold_multiset_equiv

minor tuning for release;

source files are always encoded as UTF-8;

eliminated fragile HTML.with_charset -- always use utf-8;

recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;

removed old generated stuff; removed DOS line endings;

comment;

update documentation

replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

export more information about available SMT solvers

setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;

use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."

updated generated file;

removed confusing comments (cf. 500171e7aa59);

merged

removed outdated lint script

merged

compile

run synchronous Auto Tools in parallel

really fixed comment (cf. 7abeb749ae99)

theorem names generated by the (rep_)datatype command now have mandatory qualifiers

eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended

NEWS

only instantiate type variable if there exists some in quickcheck

fixing comment in library

adapting predicate_compile_quickcheck

adding a nice definition of Id_on for quickcheck and nitpick

adding code equation for finiteness of finite types

improving sledgehammer_tactic and adding relevance filtering to the tactic

adapting mutabelle

adapting SML_Quickcheck to recent changes

explaining quickcheck testers in the documentation

adapting quickcheck examples

improving presentation of quickcheck reports

declaring quickcheck testers as default after their setup

activating construction of exhaustive testing combinators

renamed generator into exhaustive

checking if parameter is name of a tester which allows e.g. quickcheck[random]

moving iteration of tests to the testers in quickcheck

removed dead test_term_small function in quickcheck

renamed parameter from generator to tester; quickcheck only applies one tester on invocation

adding configuration quickcheck_tester

adding smart quantifiers to exhaustive testing

adapting mutabelle

only handle TimeOut exception if used interactively

removed interrupt handling that violates Isabelle/ML exception model

corrected indentation

tuned

smallvalue_generator are defined quick via oracle or sound via function package

adding shorter output syntax for the finite types of quickcheck

improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package

changed order of lemmas to overwrite the general code equation with the nbe-specific one

adapt proofs to changed set_plus_image (cf. ee8d0548c148);

bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');

updated latex dependencies (cf. 7d88ebdce380);

tuned README;

isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;

proper theory name (cf. e84f82418e09);

merged;

merged

tuned cpodef code

reformulate lemma preorder.ex_ideal, and use it for typedefs

Prove rel_interior_convex_hull_union (by Grechuck Bogdan).

merged

adapted expected value to more idiomatic numeral representation

corrected representation for code_numeral numerals

separate term_of function for integers -- more canonical representation of negative integers

merged

Use coercions in Approximation (by Dmitriy Traytel).

more antiquotations; removed some slightly outdated text;

configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;

renamed trace_simp to simp_trace, and debug_simp to simp_debug;

merged

merged

generalized simple_functionD

Moved theorems to appropriate place.

Shorter definition for positive_integral.

Move SUP_commute, SUP_less_iff to HOL image; Cleanup generic complete_lattice lemmas in Positive_Infinite_Real; Cleanup lemma positive_integral_alt;

Generalized simple_functionD and less_SUP_iff. Moved theorems to appropriate places.

Tuned setup for borel_measurable with min, max and psuminf.

Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;

give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)

merged

coercions

merged

moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.

Corrected IsaMakefile

merged

Updated NEWS

More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.

Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.

merged

use type constructor as name for variable

optional explicit prefix for type mapper theorems

file for package tool type_mapper carries the same name as its Isar command

merged

domain package generates non-authentic syntax rules for parsing only

builtin time bounds (again);

tuned;

more abstract handling of Time properties;

store tooltip-dismiss-delay as Double(seconds);

more abstract/uniform handling of time, preferring seconds as Double;

merged

NEWS

just one HOLogic.mk_comp;

more direct use of binder_types/body_type;

tuned;

simplified HOL.eq simproc matching;

tuned;

just one Term.dest_funT;

activate subtyping/coercions in theory Complex_Main;

simplified equality on pairs of types;

more precise dependencies;

two-staged architecture for subtyping; improved error messages of subtyping (using the new architecture); bugfix: constraint graph consistency check after cycle elimination;

merged

change cpodef-generated cont_Rep rules to cont2cont format

internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules

remove gratuitous semicolons from ML code

add continuity lemma for List.map

simplify predomain instances

merged

split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models

code preprocessor setup for numerals on word type; less meta-equalites; more xsymbols; less implicit propositions

merged

adaptions to changes in Equiv_Relation.thy

adapted fragile proof

adaptions to changes in Equiv_Relation.thy; prefer primrec if possible

adaptions to changes in Equiv_Relation.thy

merged

more systematic and compact proofs on type relation operators using natural deduction rules

adapted proofs to slightly changed definitions of congruent(2)

reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text

replaced slightly odd locale congruent2 by plain definition

replaced slightly odd locale congruent by plain definition

equivI has replaced equiv.intro

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules

moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition

simplify proof of LIMSEQ_unique

use new 'file' antiquotation for reference to Dedekind_Real.thy

merged

instance list :: (discrete_cpo) discrete_cpo; compactness lemmas for Nil, Cons; instance list :: (chfin) chfin;

merged

also support higher-order rules for Z3 proof reconstruction

merged

less ghc-specific pragma

tuned

updated generated files;

added document antiquotation @{file};

Parse.liberal_name for document antiquotations and attributes;

ML results: enter before printing (cf. Poly/ML SVN 1218);

merged

merged

merged

change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec

add lemma cont2cont_if_bottom

added Parse.literal_fact with proper inner_syntax markup (source position); tuned;

tuned signature;

less frequent sidekick parsing, which is relatively slow;

basic setup for bundled Java runtime;

updated reference platforms;

merged

merged

gave more standard finite set rules simp and intro attribute

more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);

added 'syntax_declaration' command;

more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;

superficial tuning;

updated versions;

recovered Isabelle2009-2 NEWS -- published part is read-only;

follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);

removed HOLCF for now as explicit component

fix cut-and-paste errors for HOLCF entries in IsaMakefile

update web description of HOLCF; fix broken link to HOLCF/index.html

remove HOLCF from build script, since it no longer works

moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;

merged

rename Pcpodef.thy to Cpodef.thy; rename pcpodef.ML to cpodef.ML;

renamed several HOLCF theorems (listed in NEWS)

rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo

rename rep_contlub lemmas to rep_lub

rename function 'match_UU' to 'match_bottom'

rename function 'strict' to 'seq', which is its name in Haskell

merged

merged

typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned

merged

merged

corrected: use canonical variables of type scheme uniformly

tuned

merged

consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings

tuned example

merged

updated generated documents

added equation for Queue; tuned proofs

added evaluation section

tuned formatting; adjustments to changes on ML level

added label

more thorough process termination (cf. Scala version);

prefer Isabelle/ML concurrency elements; more careful propagation of interrupts;

removed bash from ML system bootstrap, and past the Secure ML barrier;

more proper int wrappers;

explicit check for requirement;

more basic Isabelle_System.mkdir;

tuned;

more explicit Isabelle_System operations;

prefer Synchronized.var over CRITICAL/Unsynchronized.ref;

moved file identification to thy_load.ML (where it is actually used);

removed some old settings;

recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);

merged

remove map function names from domain package theory data

isar-style proof for lemma contI2

remove case combinator for fixrec match type

declare more simp rules for powerdomains

merged; adapted ListPair.UnequalLengths;

merged

strict forall2

nbe decides equality of abstractions by extensionality

eliminated some generated comments;

merged

merged

keep type variable arguments of datatype constructors in bookkeeping

document changes in Nitpick and MESON/Metis

renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

just one version of fold_rev2;

explicit use of unprefix;

keep private things private, without comments;

eliminated some clones of eq_list;

merged

new lemma

lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

prefer non-classical eliminations in Pure reasoning, notably "rule" steps;

discontinued global "Isabelle" symlink, to make each distribution even more self-contained;

more correct spelling;

globbing constant expressions use more idiomatic underscore rather than star

globbing constant expressions use more idiomatic underscore rather than star; precised

datatype constructor glob for code_reflect

merged

merged

merged

toplevel deresolving for flat module name space

merged

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

adjust Sledgehammer/SMT fudge factor

clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);

merge

cosmetics

eta-reduce on the fly to prevent an exception

merged

Added the simplest finite Ramsey theorem

reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions

set Metis option on correct context, lest it be ignored

make "debug" mode of Sledgehammer/SMT more liberal

fix check for builtinness of 0 and 1 -- these aren't functions

added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway

document requirement on theory import

corrected abd4e7358847 where SOMEthing went utterly wrong

merged

swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)

instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

removing Enum.in_enum from the claset

merged

be more precise: only treat constant 'distinct' applied to an explicit list as built-in

be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

announcing some latest change (d40b347d5b0b)

merged

more precise characterization of built-in constants "number_of", "0", and "1"

merged

merged

adhere established Collect/mem convention more closely

merged

replaced misleading Fset/fset name -- these do not stand for finite sets

renamed slightly ambivalent crel to effect

disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day

more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT

use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on

make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT

try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates

added "verbose" option to Metis to shut up its warnings if necessary

added support for quantifier weight annotations

share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'

added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions

generous timeout gives more breath in parallel run on less luxury machines

adding setup for exhaustive testing in example file

hiding enum

adapting example in Predicate_Compile_Examples

hiding the constants

improving function is_iterable in quickcheck

adding temporary options to the quickcheck examples

adapting the quickcheck examples

adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

adding code equations for EX1 on finite types

adding code equation for function equality; adding some instantiations for the finite types

adding Enum to HOL-Main image and removing it from HOL-Library

moving Enum theory from HOL/Library to HOL

splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck

adding prototype for finite_type instantiations

adding option finite_types to quickcheck

adding test cases for smallcheck and adding examples where exhaustive testing is more successful

changed old-style quickcheck configurations to new Config.T configurations

adding temporary function test_test_small to Quickcheck

added useful function map_context_result to signature

moving the error handling to the right scope in smallvalue_generators

removing clone from function package and using the clean interface from Function_Relation instead

adding function generation to SmallCheck; activating exhaustive search space testing

adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict

generalized ensure_random_datatype to ensure_sort_datatype

renaming quickcheck generator code to random

ported sledgehammer_tactic to current development version

adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test

adding files to use sledgehammer as a tactic for non-interactive use

adding birthday paradoxon from some abandoned drawer

adding extensional function spaces to the FuncSet library theory

tuned

tuned

updated explode vs. raw_explode;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

total Symbol.explode (cf. 1050315f6ee2);

do not export Thy_Load.required, to avoid confusion about the interface;

merged

declare adm_chfin [simp]

add lemma cont_fun; remove unused lemma monofun_app

accumulated NEWS updates for HOLCF

section -> subsection

add lemma adm_prod_case

merged

First-order pattern matching: catch a rogue exception (differing numbers of arguments)

eval simp rules for predicate type, simplify primitive proofs

generalized type

made smlnj happy

merged

proper qualification needed due to shadowing on theory merge

more appropriate name for property

mapper for sum type

mapper for option type

mapper for list type; map_pair replaces prod_fun

map_pair replaces prod_fun

mapper for mulitset type

mapper for mapping type

mapper for fset type

mapper for dlist type

map_fun combinator in theory Fun

some updates after 2 years of Mercurial usage;

mention Sledgehammer with SMT

enabled SMT solver in Sledgehammer by default

merged

keep variables bound

remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem

merged

infer variances of user-given mapper operation; proper thm storing

code eqn for slice was missing; redefined splice with fun

move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain

merged

typedef (open) unit

add bind_bind rules for powerdomains

merged

emerging Isar command interface

fixed typo

updated keywords

ML signature interface

stub for Isar command interface

module for functorial mappers

merged

require the b2i file ending in the boogie_open command (for consistency with the theory header)

use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

add lemmas about powerdomains

declare {upper,lower,convex}_pd_induct as default induction rules

rename 'repdef' to 'domaindef'

refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;

less parentheses, cf. Session.welcome;

avoid spam;

more robust determination of java executable;

init_component: require absolute path (when invoked by user scripts);

more explicit explanation of init_component shell function;

paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;

tuned message;

post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);

more reasonably defaults for typical laptops (2 GB RAM, 2 cores); enforce -server JVM if possible (NB: default JRE on Windows lacks that);

added forall2 predicate lifter

merged

merged

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

honour timeouts which are not rounded to full seconds

better error message

better error message

merged

cosmetics

interpret SMT_Failure.Solver_Crashed correctly

turn on Sledgehammer verbosity so we can track down crashes

pick up SMT solver crashes and report them to the user/Mirabelle if desired

merged

only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers

trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)

merged

ignoring the constant STR in the predicate compiler

non-executable source files;

eliminated old-style sed in favour of builtin regex matching;

more robust treatment of spaces in file names;

tuned error messages;

merged

re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)

re-generalized type of prod_rel (accident from 2989f9f3aa10)

formal dependency on b2i files

merged

check the return code of the SMT solver and raise an exception if the prover failed

updated README;

tuned;

cover 'write' as primitive proof command;

clarified interact/print state: proof commands are treated as in TTY mode to get full response;

somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";

always print state of proof commands (notably "qed" etc.);

simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

tuned message;

proper escape in regex;

report malformed symbols;

qualified Symbol_Pos.symbol;

total Symbol.source;

eliminated slightly odd pervasive Symbol_Pos.symbol;

treat Unicode "replacement character" (i.e. decoding error) is malformed;

simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);

tuned;

back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;

await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

updated README;

defensive defaults for more robust experience for new users;

merged

preliminary support for newer versions of Z3

turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

let the theory formally depend on the Boogie output

look for certificates relative to the theory

dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

merged

update Theory.requires with new theory name

tuned signatures;

never open Unsynchronized;

merged

section headings

reorder chapters for generated document

merge Representable.thy into Domain.thy

move stuff from Domain.thy to Domain_Aux.thy

move map functions to new theory file Map_Functions; add theory file Plain_HOLCF

allow unpointed lazy arguments for definitional domain package

add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

merged

removed unused lemma chain_mono2

rename class 'bifinite' to 'domain'

instance sum :: (predomain, predomain) predomain

configure sum type for fixrec

add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)

instance prod :: (predomain, predomain) predomain

adapt isodefl proof script to unpointed types

add 'predomain' class: unpointed version of bifinite

add bifiniteness check for domain_isomorphism command

implement map_of_typ using Pattern.rewrite_term

avoid using stale theory

implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data

add function the_sort

refactor tmp_thy code

reorganize Bifinite.thy; simplify some proofs related to bifinite class instances

treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;

Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;

more precise treatment of deleted nodes;

tuned error message;

unified type Document.Edit;

replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;

tuned;

reduced danger of line breaks within minipage;

Sidekick block asset: show first line only;

added buffer_text convenience, with explicit locking;

use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);

merged

make SML/NJ happy

merged

slightly changed fun_map_def

fun_rel_def is no simp rule by default

more appropriate specification packages; fun_rel_def is no simp rule by default

type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions

more appropriate specification packages; fun_rel_def is no simp rule by default

type annotations in specifications; fun_rel_def is no simp rule by default

fun_rel_def is no simp rule by default

merged

tidied using metis

manage folding via sidekick by default;

eliminated obsolete heading category -- superseded by heading_level;

treat main theory commands like headings, and nest anything else inside;

proper treatment of equal heading level;

added missing Keyword.THY_SCHEMATIC_GOAL; more keyword categories;

default Sidekick parser based on section headings;

some support for nested source structure, based on section headings;

tuned;

misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);

updated version;

private counter, to keep externalized ids a bit smaller;

added general Synchronized.counter convenience;

explicitly identify forked/joined tasks;

accomodate old manuals that include pdfsetup.sty without isabelle.sty;

merged

removed type-inference-like behaviour from relation_tac completely; tuned

avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);

explicitly check uniqueness of symbol recoding;

more hints on building and running Isabelle/jEdit from command line;

merged

merge

reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving

merged

merged

(infixl "<<" 55) -> (infix "<<" 50)

simplify some proofs

remove unnecessary stuff from Discrete.thy

remove some unnecessary lemmas; move monofun_LAM to Cfun.thy

add lemma eq_imp_below

discontinue a bunch of legacy theorem names

move a few admissibility lemmas into FOCUS/Stream_adm.thy

simplify some proofs

compile -- 7550b2cba1cb broke the build

merge

recognize Vampire error

return the process return code along with the process outputs

better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)

merged

corrected slip: must keep constant map, not type map; tuned code

constructors to datatypes in code_reflect can be globbed; dropped unused code

adding code and theory for smallvalue generators, but do not setup the interpretation yet

make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice

better detection of completely irrelevant facts

always use a hard timeout in Mirabelle

use "smt" (rather than "metis") to reconstruct SMT proofs

don't pass too many facts on the first iteration of the SMT solver

catch TimeOut exception

ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed

removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway

make Nitpick datatype tests faster to make timeout less likely

invoke SMT solver in a loop, with fewer and fewer facts, in case of error

always honor the max relevant constraint

more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;

updated generated files;

tweaked pdf setup to allow modification of \pdfminorversion;

merged;

updated generated files;

basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;

updated generated file;

more literal appearance of antiqopen/antiqclose;

'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);

continue after failed commands;

added Keyword.is_heading (cf. Scala version); tuned;

updated keywords;

mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;

somewhat more uniform timing markup in ML vs. Scala;

somewhat more uniform timing in ML vs. Scala;

added Markup.Double, Markup.Double_Property; tuned;

explicit "timing" status for toplevel transactions;

tuned;

tuned comments;

abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical

moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;

updated keywords;

reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;

eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; more uniform shortlogentry and filelogentry;

reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;

obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);

explicit indication of some remaining violations of the Isabelle/ML interrupt model;

updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;

proper spelling; proper format;

merged

Extend convex analysis by Bogdan Grechuk

merged

fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)

make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

pass proper type to SMT_Builtin.is_builtin

remove " s" suffix since seconds are now implicit

ignore facts with only theory constants in them

cosmetics

use the SMT integration's official list of built-ins

added class relation group_add < cancel_semigroup_add

merged

changing timeout to real value; handling Interrupt and Timeout more like nitpick does

added two lemmas about injectivity of concat to the list theory

adding documentation of some quickcheck options

merged

Code.check_const etc.: reject too specific types

corrected quoting

added lemma length_alloc

dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document

added note on countable types

simulate more closely the behaviour of the tactic

merged

merged

merged

dropped debug message

more precise text

SMLdummy target

fixed typos

moved theory Quicksort from Library/ to ex/

Theory Multiset provides stable quicksort implementation of sort_key.

added code lemmas for stable parametrized quicksort

tuned proof

moved file in makefile to reflect actual dependencies

give E one more second, to prevent cases where it finds a proof but has no time to print it

use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs

don't be overly verbose in Sledgehammer's minimizer

standardize on seconds for Nitpick and Sledgehammer timeouts

cleaned up

added property "tooltip-margin";

clarified tooltips: message output by default, extra info via control/command;

warn in correlation with report -- avoid spurious message duplicates;

tuned;

feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);

merged

updated SMT certificates

standardize timeout value based on reals

merged

merged

change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'

merged

renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun

renamed lemma cont2cont_Rep_CFun to cont2cont_APP

simplify proof of typedef_cont_Abs

rename constant trifte to tr_case

add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'

make syntax of continuous if-then-else consistent with HOL if-then-else

rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff

polyml_as_definition does not require explicit dependencies on external ML files

explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;

discontinued obsolete function sys_error and exception SYS_ERROR;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

try_param_tac: plain user error appears more appropriate;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

eliminated dead code;

more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;

removed assumption

more on naming tactics;

merged

merged

tuned proof

tuned proof

tuned lemma proposition of properties_for_sort_key

lemmas sorted_map_same, sorted_same

lemmas multiset_of_filter, sort_key_by_quicksort

more on "Time" in Isabelle/ML;

simplified some time constants;

added convenience operation seconds: real -> time;

avoid catch-all exception handling;

eliminated fragile catch-all pattern, based on educated guess about the intended exception;

Attribute map_function -> coercion_map; tuned;

syntax category "real" subsumes plain "int";