attempt to run without ISABELLE_GHC setting again on mac-poly

apparently, setting ISABELLE_GHC makes ghc unusable

reverse induction over nonempty lists

more appropriate postprocessing of rational numbers: extract sign to front of fraction

doc fixes (contributed by Christian Sternagel)

made SML/NJ happier

avoid duplicate fact name

afp-poly runs on macbroy2 (different ghc)

reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space

tuned

register tree with datatype_compat ot support QuickCheck

fix bug caused by bad context

add mk_Trueprop_mem utility function

disabled MaSh for the Isabelle2014 release, due to a couple of issues

refactor commonly used functions

document property 'rel_sel'

generate 'rel_sel' theorem for (co)datatypes

fix rel_cases

made SML/NJ happier

add ISABELLE_GHC settings for isatest

mira.py: building jEdit plugin is required for makeall

took out 'rel_cases' for now because of failing tactic

record MaSh algorithm in spying data

tuned whitespace (also in strings)

also learn when 'fact_filter =' is set explicitly

no warning in case MaSh is disabled

don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic

no need for 'mash' subdirectory after removal of Python program

fix typo

throw error for bad input

catch "not found" case

merge

don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax

tuning

made SML/NJ happier

reactivate session Quickcheck_Examples

adapt and reactivate Quickcheck_Types and add two test cases

more docs

lambda-lifting for Z3 Isar proofs

append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)

avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)

merged

added lemmas

improved docs

made SML/NJ happier

got rid of a pointer equality

get rid of some pointer equalities

tuned terminology

improvements to the machine learning algos (due to Cezary K.)

added lemma

refactor some tactics

refactor some tactics

add helper function map_prod

document property 'rel_cases'

generate 'rel_cases' theorem for (co)datatypes

update for release;

Added tag Isabelle2014-RC0 for changeset 251ef0202e71

merged

modernized definitions;

proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);

CONTRIBUTORS

refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply; uniform appearance of xsymbol and HTML output for sums

misc tuning for release;

tuned;

NEWS

prefer ac_simps collections over separate name bindings for add and mult

added Tom's hyp_subst update

reduced name variants for assoc and commute on plus and mult

tuned;

insist in explicit overloading;

more uniform names;

misc tuning for release;

revived unchecked theory (see cebaf814ca6e);

suppress completion of obscure keyword;

tuned;

misc tuning for release;

NEWS;

Tail recursion no longer supported by "function".

merged

weaker assumption for "list_emb_trans"; added lemma

added monotonicity lemma for list embedding

no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)

renamed "list_hembeq" into slightly shorter "list_emb"

misc tuning;

merge

document property 'rel_intros'

generate 'rel_intros' theorem for (co)datatypes

Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.

tuned grammar and spelling (cf. 0cf15843b82f);

document property 'corec_code'

generate 'corec_code' theorem for codatatypes

modernized definitions;

misc tuning and clarification;

check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;

optional exit hook for theory-like targets

restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game

centralized (ad-hoc) switching of targets in named_target.ML

add lemmas: polynomial div/mod distribute over addition

reverted 9512b867259c -- appears to break 'metis'

clarified "axiomatization" -- minor rewording of this delicate concept;

tuned;

more on ML options; suppress somewhat old Pretty.margin_default;

redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;

overdue NEWS concerning c4daa97ac57a

Merge

for new release

merge

document property 'rel_induct'

generate 'rel_induct' theorem for datatypes

fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too

added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'

whitespace tuning

robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)

use context instead of theory

fine-tuned methods

tuned message

updated docs

changed default MaSh engine

removed needless code

speed up MaSh a bit

mix NB and kNN

tuned (reordered) code

clean up MaSh export a bit

clean up MaSh evaluation driver

merged

tuned;

clarified quasi-generic PIDE;

misc updates for release;

more release notes;

Library/Tree: bst is preferred to be a function

Library/Tree: use datatype_new, bst is an inductive predicate

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

some lemmas about the indicator function; removed lemma sums_def2

generate type correct terms in uncheck phase

updated to sumatra_pdf-2.5.2;

ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);

removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;

tuned comments;

updated README;

"isabelle tty" is superseded by "isabelle console";

tuned description: fit into 80 chars terminal;

qualified String.explode and String.implode

removed non-existing MaSh component from list

modernized diagnostic options

use SMT2

compile

tuning

killed Python version of MaSh, now that the SML version works adequately

tracing facilities for the code generator preprocessor

tuned interface

corrected handled exception

proper trading of variables; more appropriate ML variable names

modernized

jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;

removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);

updated NEWS -- removed material that is already in the manual;

merged

misc tuning;

misc tuning;

CONTRIBUTORS

fact consolidation

more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;

merged

command 'print_term_bindings' supersedes 'print_binds';

Proof General legacy;

removed obsolete "isabelle unsymbolize";

minor renovation of slightly odd and old README;

sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;

tweaking

correctly take weights into consideration

tuned whitespace and parentheses

use right theory name for theorems in evaluation driver

killed dead code

reintroduced 'extra features' + only print message in verbose mode

got rid of hard-coded weights, now that we have TFIDF

tuning

tuning

reintroduced 'extra features' but with lower weight than before (to account for tfidf)

resolution modulo double negation

compile

merged two small theory files

tuned variable names

whitespace tuning

repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side

tiny refinements

suppress documentation "how_to_prove_it" for now, notably for release;

updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;

updated generated file;

merged

updated cygwin on server; include unzip, which is required for src/Doc/JEdit;

tuning

reintroduced MaSh hints, this time as persistent creatures

always expand all paths

tuned output

tuned output

right array indexing

incremental learning when learing several facts

tuning

more incremental learning of single fact

avoid needless (trivial) reordering on load

recompute learning data at learning time, not query time

imported patch killed_num_known_facts0

refactoring

renamed experimental learning engines

tuning

refactoring

removed experimental machine learning engine

store string-to-index tables in memory

disable 'extra' feature tainting for now

tuning

tuning

tuning

tuning

tuning

honor visible in SML naive Bayes

honor visibility in SML k-NN

got rid of a few experimental options

tuning

killed dead code

avoid subscripting array with ~1

killed dead data

new version of adaptive k-NN with TFIDF

refactoring

tuning

refactoring

adaptive k-NN

avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)

generate right dependencies in MaSh driver

more on "Futures"; removed obsolete comments;

more on "Futures";

more on "Future values";

more on "Lazy evaluation";

more on syntax phases; tuned;

more on syntax phases;

tuned;

tuned;

tuned;

tuned;

tuned;