add lemmas

add lemmas

merged

rewrite: tuned code, no semantic changes

rewrite: with asm pattern, propagate also remaining assumptions to new subgoals

rewrite: do not descend into conclusion of premise with asm pattern

rewrite: with asm pattern, try all premises for rewriting, not only the first

tuned

rewrite: propagate premises to new subgoals

reformat comments

rewr_cconv: ignore premises when tuning conclusion

enable \<hole> syntax for rewrite

call Goal.prove only once for a quadratic number of theorems

predicate compiler: ignore Abs_filter and Rep_filter

merged

moved _aux functions from AFP/Collections to AList

merged

replace Filters in NSA by HOL-Filters

move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

add cofinite filter

add frequently as dual for eventually

add quantifier syntax for eventually

move filters to their own theory

fix latex in Transcendental

proper site for Cygwin setup;

less ambitious collection of quasi-generic PIDE modules;

tuned;

autorebase.bat.done no longer exists in Cygwin 1.7.35 -- lets hope that its incremental rebasing works for us;

merged

tuned -- avoid ML warnings;

avoid redundant shell process;

clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]

tuned;

merged

proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);

tuned whitespace;

Merge

Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

Merge

Merge

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

updated for release;

updated for release;

Added tag Isabelle2015-RC0 for changeset 42d34eeb283c

more uniform Isabelle_System.mkdirs in ML/Scala; avoid odd permission problems on Windows (e.g. Desktop) by using "mkdirs" from Cygwin;

updated for release;

tuned;

tuned spelling;

misc tuning for release;

make SML/NJ more happy;

make SML/NJ more happy;

tuned;

updated Cygwin near 1.7.35-1;

have 'primrec' return definitions

renamed ML funs

generalized code a bit

generalized code

exported function (for symmetry)

merged

renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset

tuned proofs;

tuned signature;

tuned;

renamed misleading option

obsolete;

make SML/NJ more happy;

merged

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

tuned signature

fixed typo in function name

removed a refute example that caused trouble with testing

introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)

merged

conversion between division on nat/int and division in archmedean fields

replace almost_everywhere_zero by Infinite_Set.MOST

option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;

tuned signature;

misc tuning for release;

merged

eliminated suspicious Unicode character;

eliminated hard tabs;

more standard access to goal state;

more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;

added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);

proper test for session HOL-Library;

tuned;

tuned signature;

proper context for Object_Logic operations;

explicitly checked alpha conversion -- actual renaming happens outside kernel;

more standard access to specific subgoal;

tuned wording

updated 'old_smt' to loss of 'z3_non_commercial' option

Z3 news

updated certificates to latest Z3 (and took out one problem that no longer works)

updated docs to reflect actually run ATPs

reorder provers to reflect current eval results

updated docs to Z3 open source

updated SMT module and Sledgehammer to fully open source Z3

updated to new Z3

renamed multiset ordering to free up nice <# etc. symbols for the standard subset

removed TODO

consistent naming

merged

more lemmas and operations on cset (adapted from FSet)

tuned signature;

tuned;

misc tuning for release;

merged

Removed mcard because it is equal to size

generalized slightly

generalized code

generalized code

export ML function

recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;

more qualified names -- eliminated hide_const (open);

tuned;

merged

local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;

support for 'restricted' modifier: only qualified accesses outside the local scope;