updated CONTRIBUTORS

updated NEWS

document option

merged "isar_try0" and "isar_minimize" options

hardcoded obscure option

hard-coded an obscure option

use configuration mechanism for low-level tracing

moved focus to Isabell/jEdit and away from Proof General

took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired

tuning (use a blacklist instead of a whitelist)

reduce the number of emitted MaSh commands (among others to facilitate debugging)

MaSh tweaks to facilitate debugging

tuned proofs

make SML/NJ happy

renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")

more primcorec docs

added primcorec examples with lambdas

more primcorec docs

adapted primcorec documentation to reflect the three views

updated docs

took out spurious attributes (no need for several code equations / simps for thesame constants)

have "datatype_new_compat" register induction and recursion theorems in nested case

prefer Code.abort over code_abort

setting the stage for safe constructor simp rules

added TODO

made tactic more reliable

killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'

cleaner handling of collapse theorems

repaired latex (cf. 84522727f9d3);

updated NEWS

dropped dead code

don't declare ctr view primcorec theorems as simp (they loop)

simplified code; eliminated some dummyTs

avoid infinite loop for unapplied terms + tuning

generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"

give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"

added auxiliary function

avoid parameter

added helper function for code equations in primcorec

updated NEWS and CONTRIBUTORS

split functionality into two functions to avoid redoing work over and over

added massaging function for primcorec code equations

simplified code

no need for beta-eta contraction

generalize helper function

generate more theorems (e.g. for types with only one constructor)

added two functions to List (one contributed by Manuel Eberl)

generate constructor view theorems

merged;

merged;

tuned proofs;

tuned proofs;

added option "jedit_auto_load"; allow in-place change of option "editor_continuous_checking";

limit for text height;

improved layout, with special treatment for ScrollPane;

tuned signature;

improved FlowLayout for wrapping of components over multiple lines;

updated to polyml-5.5.1;

improved printing of exception trace in Poly/ML 5.5.1;

more antiquotations; tuned signature;

moved module into plain Isabelle/ML user space;

more primcorec tactics

enrich data structure

include more "discI" rules

updated docs

tuning (alphabetical order)

removed spurious "simp"

note "discI"

tuned tactics

no need thanks to "Code.abort"

minor change related to code equations in primcorec

don't unfold as eager as in 11a77e4aa98b

tuned proofs

use singular to avoid confusion

new tactics for constructor view

tuning

fixed embarrassing typo in example

avoid duplicate simp rule warnings

added and tuned lemmas

tuned proofs;

updated to official polyml-5.5.1;

updated to polyml-5.5.1; prefer explicit POLYML_HOME to simplify additional user settings;

actually use x86_64 machine;

correct merging of restore data

order_bot, order_top

include Int_Pow into Quotient_Examples; add end of the theory

NEWS: Simps_Case_Conv

added lemmas and made concerse executable

merge

return right theorems

more (co)data docs

tuned proofs about 'convex'

more (co)data docs

tuned proofs;

treat all dummy type variables separately (in contrast to fca432074fb2);

removed dead code (see also 69d4543811d0);

merged

tuned signature;

more antiquotations -- avoid unchecked string literals;

more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);

distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions; some notes about missing ML interface;

tuned white space; avoid "object-oriented English";

adhoc check of ML sources, in addition to thy files already covered in Thy_Load;

proper Isabelle symbols -- no UTF8 here;

proper Cygwin mirror for Isabelle2013-1;

explicit test of quick_and_dirty, which is rarely used in practice;

updated to cygwin-20130916;

more CHECKLIST;

updated cygwin snapshot;

updated to smlnj 110.76;

prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);

more NEWS;

merge

prove simp theorems for newly generated definitions

example using restoring Transfer/Lifting context

use lifting_forget for deregistering numeric types as a quotient type

restoring Transfer/Lifting context

make ML function for deleting quotients public

public access to the raw transfer rules - for restoring transferring

another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;

more (co)data docs

more (co)data docs

added missing theorems to "simps" collection

more (co)data docs

more (co)data docs

more (co)data docs

merged

tuned proofs;

tuned magic number, for improved reactivity on old 2-core machine;

tuned proofs;

updated keywords

tuned proof

merged

tuned proofs;

print find_thms result in reverse order so best result is on top

more useful sorting of find_thms results

proper sharing after change of directory structure (cf. 32ec957e5c3e); result is structurally equal, despite change of hash key;

restricted heap, which might improve stability of this test;

merged

tuned proofs;

tuned proofs;

updated to jdk-7u40;

added component jdk-7u40.tar.gz (inactive);

merged

more (co)data docs

tuning

more (co)data doc

generalized and simplified proofs of several theorems about convex sets

more (co)data docs

removed accidentally submitted line

more (co)data doc

more general typing of monadic bind

merged

omit automatic Induct.cases_pred declaration, which breaks many existing proofs

NEWS and CONTRIBUTORS

merged

added some examples and tests for fun_cases

dropped unnecessary 'open'

tuned headers

moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information; normalized whitespace and indentation

clarified

clarified, dropping unreachable bool special case

dropped dead code

clarified

generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)

tuned proofs

merged

make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'

generalize lemmas

remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)

remove duplicate lemmas

new lemmas

prefer theorem name over 'long_thm_list(n)'

prefer attribute 'unfolded thm' to 'simplified'

removed outdated comments

made non-co case more robust as well (cf. b6e2993fd0d3)

don't wrongly destroy sum types in coiterators

beware of multi-constructor datatypes (cf. 27c418b7b985)

beware of single-constructor datatypes, with no discriminators

more robust tactic to cover another corner case (added as example);

generalized data structure, for extension with SMT solver proofs

prefixed types and some functions with "atp_" for disambiguation

merged;

absorb final CLASSPATH as well, such that tools might provide that by elementary means, without the "classpath" shell function (e.g. kodkodi/nitpick);

more CHECKLIST;

more robust System.getProperty with default;

generate distribution classpath for cold-start application wrappers;

reverse orientation of ISABELLE_CLASSPATH;

propagate ISABELLE_CLASSPATH;

tuned comments;

clarified directory structure;

maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources); ignore $ISABELLE_JAVA_EXT -- do not change java.ext.dirs;

more official initial class path according to sun.misc.Launcher;

provide main classpath again, notably for cold-start;

cold-start of main application even on Linux;

tuned proofs;

more explicit indication of 'done' as proof script element;

made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"

conceal definitions of high-level constructors and (co)iterators

conceal low-level noted facts (+ FIXME to get rid of the notes altogether eventually)

buffer the notes even more

conceal internal bindings

add a notice to myself in doc

more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses

unset some spurious executable flags

handle corner case in tactic

simplified derivation of in_rel

removed unused/inlinable theorems

when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated

minor fixes

commented out code parts leading to runtime errors due to missing gensim module

invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)

new version of MaSh

more (co)data docs

avoid a keyword

more (co)datatype docs

killed dead code

get rid of another complication in relevance filter

tuning

renamed config option

more correct NEWS

kick out totally hopeless facts after 5 iterations to speed things up

reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

more (co)data docs

more (co)data docs

more (co)data docs

merged

prefer explicit type constraint (again, see also Type.appl_error); pretty const with markup; clarified "the context";

tuned signature;

tuned whitespace;

tuned message;

do not expose internal flags to attribute name space;

more (co)data docs

more (co)datatype documentation

tuning

disable some checks for huge background theories

tuning

reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)

reverted f99ee3adb81d -- that old logic seems to make a difference still today

merged