tuned;

merged

tuned proofs;

tuned signature;

tuned signature -- clarified Proof General legacy;

toplevel function "use" refers to raw ML bootstrap environment;

obsolete;

proper thy_load command 'boogie_file' -- avoid direct access to file-system;

tuned signature;

updated example;

prefer UTF8.decode_permissive;

more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;

more specific Protocol_Output: empty message.body, main content via bytes/text;

tuned imports;

tuned signature;

immutable byte vectors versus UTF8 strings;

dropped duplicate of of_bool

proper code equations for Gcd and Lcm on nat and int

tuned

fixed type variable confusion in 'datatype_new_compat'

implemented 'tptp_translate'

reintroduced (unimplemented) 'tptp_translate' tool

have MaSh support nameless facts (i.e. proofs) and use that support

made SML/NJ happy

renamed thm

explicit inclusion of data refinement theory into HOL-Library session

tuned to improve automation (for REPEAT)

separated comparision on bit operations into separate theory

prohibit locally fixed type variables in bnf definitions

tuned

standard relator for list bnf

tuned example

shortened generated property name

more explicit syntax for defining a bnf

fix document generation for HOL-Probability

fix document generation for Extended_Nat

measure of a countable union

add restrict_space measure

better support for enat and ereal conversions

enat is countable

add equalities for SUP and INF over constant functions

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

add acyclicI_order

stronger inc_induct and dec_induct

countability of the image of a reflexive transitive closure

support of_rat with 0 or 1 on order relations

equation when indicator function equals 0 or 1

ported part of function package to new 'Ctr_Sugar' abstraction

undid copy-paste

ported 'partial_function' to 'Ctr_Sugar' abstraction

port list comprehension simproc to 'Ctr_Sugar' abstraction

added convenience function

document idiomatic use of 'simps_of_case'

ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

register old-style datatypes as 'Ctr_Sugar'

export useful ML function

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

tuned headers

moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction

updated sessions;

proper latex -- NB: cannot use antiquotation here;

merged

simplified App template;

obsolete;

obsolete;

tuned message;

tuned signature -- removed obsolete Addsimprocs, Delsimprocs;

tuned signature;

minor doc fix

merged

merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;

removed obsolete RC tags;

Added tag Isabelle2013-1 for changeset 9c1f21365326

tuned;

more on completion;

adjust modules for Admin/build jars_test;

tuned whitespace;

added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);

transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;

Added tag Isabelle2013-1-RC4 for changeset 594628261376

updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);

tuned;

misc tuning;

updated to jedit_build-20131106 (Console.jar 5.1.3);

join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;

tuned signature;

less tiny font for search criteria;

tuned tooltips;

swap equations and premises in the coinductive step for better proof automation

no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;

tuned;

CONTRIBUTORS

more on text completion;

tuned;

more on Monitor panel;

more on Timing;

more on miscellaneous tools;

more screenshots;

more screenshots;

more on Sledgehammer; more on Find;

more on automatically tried tools;

more on prover output; more sections;

misc tuning and clarification;

more on file-system access; provide ISABELLE_HOME_USER as well;

tuned;

more on problems and workarounds;

tuned;

clarified isabelle options -l;

tuned;

clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);

removed dead code (see also db4bf4fb5492);

Added tag Isabelle2013-1-RC3 for changeset fbcaa9f08879

avoid non-portable int constant -- make SML/NJ happy;

avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;

prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;

basic IO buffer size like for fifo -- imitate implicit flushing behaviour more closely;

removed junk (cf. 409d7f7247f4);

fix a citation

declare Quotient_Examples/FSet.thy as almost obsolete

update documentation of important public ML functions in Lifting

update documentation of Lifting/Transfer and Quotient

don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.

tuned;

more screenshots; tuned;

tuned;

misc tuning;

more strict find_command -- avoid invalid hyperlink_command;

more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;

obsolete;

clarified Editor.current_command: allow outdated snapshot; more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

make double sure that AWT/Swing antialiasing is enabled (see also http://www.jedit.org/users-guide/jvm-options.html and jdk/src/share/classes/sun/awt/SunToolkit.java);

more documentation;

more documentation;

more documentation;

tuned;

NEWS;

avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);

add congruence rule to prevent code_simp from looping

Added tag Isabelle2013-1-RC2 for changeset 782e430e6a83

native executable for Linux (see Admin/Linux);

proper NULL termination;

native executable even for Linux, to avoid surprises with file managers opening executable script as text file;

proper warning at run time, not in the parser;

prefer "fresh" open -- requires Lion / Mountain Lion;

clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;

prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)

more parallelism in blocking mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

another shortcut alias;

NEWS;

Added tag Isabelle2013-1-RC1 for changeset c37100233af7

reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code

removed dead code

added check to avoid odd situations the N2M code cannot handle

reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)

tuned signature

handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)

tuned

tuned

qualifed popular user space names

dropped obsolete check: dest_num always yields positive number

simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

more exercises

by (auto ...)[1] not by (auto [1])

added exercise

Add output translation for <a := .., b := .., ..> state notation.

reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)

more docs

properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel

reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP

simplified code

fourth attempt at generalizing N2M types (to leverage caching)

tuning

int and nat are conditionally_complete_lattices

be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'

removed dead code

update docs

take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case

took out loopy code

take out even less aggressive generalization -- it's still too aggressive

reverted too aggressive 7cb8442298f0

generalize more aggressively

avoid subtle failure in the presence of top sort

tuning

get mutually recursive maps as well

tuned proofs in Approximation

fixed subtle name shadowing bug

use right permutation in 'map2'

stronger normalization, to increase n2m cache effectiveness

make local theory operations non-pervasive (makes more intuitive sense)

NEWS

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

generalize bdd_above/below_uminus to ordered_ab_group_add

restrict Limsup and Liminf to complete lattices

use INF and SUP on conditionally complete lattices in multivariate analysis

add SUP and INF for conditionally complete lattices

use bdd_above and bdd_below for conditionally complete lattices

generalize SUP and INF to the syntactic type classes Sup and Inf

added some N2M caching

also generalize fixed types

generalize types when synthetizing n2m (co)recursors, to facilitate reuse

nicer error message in case of duplicates

use int example like in the rest of IMP (instead of nat)

dropped dead code

fact generalization and name consolidation

streamlined setup of linear arithmetic

make 'try0' return faster when invoked as part of 'try'

careful with lists of different lengths

split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')

better error handling

more robust treatment of dead variables in n2m

more robust n2m w.r.t. 'let's

tuning

strengthened tactic

made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)

handle constructor syntax in n2m primcorec

typo

made sugared 'coinduct' theorem construction n2m-proof

moved code around

tuning

make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)

conceal definition

more exercises

more exercises

more simplification rules on unary and binary minus

generate stable names for axioms

purely algebraic foundation for even/odd

moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger

explicit type class for modelling even/odd parity

generalized of_bool conversion

separated bit operations on type bit from generic syntactic bit operations

restructed

generalised lemma

more lemmas on division

more convenient place for a theory in solitariness

consolidated clone theory

more exercises

tuned text

inst_lift now fully instantiates context to avoid problems with loose bound variables

include corecursive functions' arguments in callssss

more exercises

merged

more exercises

commented out vaporware

more exercises

tuning

tuning

tuned names (to make them independent from temporary naming convention used in characteristic theorems)

align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')

convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'

tuned error message

more exercises

handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)

tuning

more correct (!) types for recursive calls

watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')

got rid of annoying duplicate rewrite rule warnings

use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations

refactored rtrancl_while; prove termination for finite rtrancl

more exercises

added exercises

added 'primcorec' examples

tuned

removed junk

update doc according to c0186a0d8cb3

define a trivial nonemptiness witness if none is provided

made lower-level function available

more doc -- feedback from Andrei P.

added exercise

more docs

more docs

more docs

expand doc a bit

updated doc

tuning

warn about incompatible recursor signature

more informative abort

tuning

systematically close derivations in BNF package

removed temporary error handling

strengthened tactic

tuning

reintroduced parts of 07a8145aaeba that a22ded8a7f7d wrongly took out

tuning

gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation

tuning

tuning

tuning

tuning

simplify code

avoid tactic failure for equations that contain an unapplied 'id'

improve support for recursion through functions

handle composition for multiple arguments correctly

merge

generate callssss

set stage for more flexible 'primrec' syntax for recursion through functions

don't print BNF constants

tuning

conceal even more ugly constructions

conceal more ugly constructions

conceal prim(co)rec definitions

avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'

updated docs

set code attribute on discriminator equations

MaSh error handling

repair invariant in MaSh when learning new proofs

killed more "no_atp"s

killed most "no_atp", to make Sledgehammer more complete

doc fixes suggested by Andreas L.

make sure that registered code equations are actually equations

accept very long lines in MaSh

make sure add: doesn't add duplicates, and works for [no_atp] facts

no fact subsumption -- this only confuses later code, e.g. 'add:'

generate a comment storing the goal nickname in "learn_prover"

clarified message

added thread-safety warnings

avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk

handle nested tuples in 'let's

more exercises

also unfold let (_, _) = ... syntax

added helper function (that solves chicken-and-egg problem w.r.t. "callssss")

graceful handling of abort

generalized interface

choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first

thread the goal through instead of relying on unreliable (possibly fake) state

added comment

tuning

verbose minimization when learning from ATP proofs

if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice

if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"

fast track -- avoid domain error in 0 case

remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'

merged

tuned exercises

use Code.abort instead of undefined in auto-generated equations

have MaSh minimize

tweaked signature

strengthened tactic to deal with 'False ==> ...'

made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms

improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance

updated S/H docs

use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available

drop only real duplicates, not subsumed facts -- this confuses MaSh

renamed relcomp_def to relcomp_unfold

fixed thm names

addressed rare case where the same symbol would be treated alternately as a function and as a predicate -- adding "top2I top_boolI" to a problem that didn't talk about "top" was a way to trigger the issue

added Nitpick limitations to docs

more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder

keep temporary error handling in there until code equations are properly generated

tuning (simplified parts of 92c5bd3b342d)

tuning

stengthened tactic to cope with abort cases

tuned names

strengthened tactic w.r.t. "let"

more prominent MaSh errors

compile -- fix typo introduced in 07a8145aaeba

pass the right theorems to tactic

prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.; generate code-style theorems (currently commented out since this still fails for many cases); filter tautologies (False ==> ...) out of generated theorems;

repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

simplify fudge factor code

cleanup SMT-related config options

no isar proofs if preplay was not attempted

normalize more equalities

parallelize MeSh

run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway

use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)

minor performance tuning

use plain types instead of dedicated type pattern

duplicate term and type patterns

optimized built-in const check

added TODO

crank up limit a bit -- truly huge background theories are still nearly 3 times larger

higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"

minor fact filter speedups

more gracefully handle huge theories in relevance filters

handle huge MaSh requests gracefully

further optimization in relevance filter

further speed up duplicate elimination

more efficient theorem variable normalization

strengthened constructor-view tactic to deal with 'let's

allow 'let's around constructors in constructor view

reword abstract

more primcorec docs

minor doc fix

new topological lemmas; tuned proofs

strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)

generate optimized DNF formula

rationalized negation code

honor externally set MASH_PORT

process code-style inputs

more tracing

more thorough spying

more Sledgehammer spying -- record fact indices

prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)

removed pointless special case

run fewer provers in "try" mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

more parallelism in blocking mode

more robustness in MaSh

back to post-release mode -- after fork point;

tuned;

tuned;

more notes;

tuned;

added and generalised lemmas

Streamlined locales reference material.

merged

tuned

merged

keep the qualification of bindings when noting bnf theorems

strengthened tactic (primcorec_sel_tac) + tuning

renamings

got rid of needless argument

make SMT integration slacker w.r.t. bad apples (facts)

strengthen top sort check

tuned whitespace;

tuned;

unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;

updated to scala-2.10.3;

tuned;

some highlights of Isabelle2013-1 based on NEWS;

tuned;

misc tuning for release;

more (co)data docs

don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded

NEWS and CONTRIBUTORS

made SML/NJ happy

use new coinduction method and primcorec in examples

new coinduction method

tuned command descriptions

strengthen tactic w.r.t. let

minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)

typo

NEWS and CONTRIBUTORS

merged

compile -- broken since 21dac9a60f0c

strengthened tactic for right-hand sides involving lambdas

basic documentation for function elimination rules and fun_cases

allow uncurried lambda-abstractions on rhs of "primcorec"

tiny doc fix

base the fset bnf on the new FSet theory

improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.)

removed spurious save if nothing needs to bee learned

new version of MaSh that really honors the --port option and that checks for file name mismatches

minor textual changes

got rid of dead feature

refactoring -- splitting between constructor sugar dependencies and true BNF dependencies

renamed ML files

renamed theory file

tuned signature -- facilitate experimentation with other processes;

preserve types during rewriting

made SML/NJ happy

made SML/NJ happy

made SML/NJ happier

added experimental configuration options to tune use of builtin symbols in SMT

added possibility to reset builtins (for experimentation)

just one data slot (record) per program unit

more "primrec_new" documentation

merged

tuned signature;

eliminated clone of Inductive.mk_cases_tac;

tuned signature;

tuned whitespace;

provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);

merge

minor tweak to error message

tuned;

explicit caret position after replacement;

tuned proofs

observe user preferences;

updated for release;

tuned;

tuned;

more on text completion;

made SML/NJ happy (NB: toplevel ML environment is unmanaged);

updated for release;

updated for release;

updated to sumatra_pdf-2.3.2;

low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;

backout c6297fa1031a -- strange parsers are required to make this work;