tuned

check for correct proof output

fixed: count constants with supplementary lemmas

removed latex markup - there is no document generated from Decision_Procs/ex

Implemented taylor series expansion for approximation

renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;

merged

more display;

added icon;

basic launch4j setup;

fixed permissions;

fixed permissions;

Corrected handling of bound variables.

merged

dropped Id

explicit Set constructor for code generated for sets

hide popular names

Executable_Set is now a simple wrapper around Fset

renamed theory Code_Set to Fset

updated generated document

Executable_Set now based on Code_Set

added Inter, Union

more precise dependencies for "jars"; allow spaces in SCALA_HOME;

improved display;

display some platform information;

discontinued separate "pdf" archive -- since it is now relatively small compared to the main archive, there is no point to fragment things; adaptation replaces adaption (cf. 555b56b66fcf);

merged

check if conjectures have been used in proof

return number of first conjecture-clause and number of conjecture-clauses;

use structure File instead of TextIO; removed comments

whitelist for HOL problems with ext: as a 'helper clause' ext was not passed to metis, but metis does not include ext

always include whitelist;

check for current versions on server

relevance filter with the same parameters for remote-versions

use X2TPTP optionally and only for remote_spass; append original response if proof is extracted

fixed

clarified "jars" target;

produce self-contained isabelle-scala.jar;

proper interpretation of Cygwin.config;

sane platform look-and-feel;

minimal GUI_Setup, which is the main class of Pure.jar;

some more Cygwin checks;

moved platform identification to platform.scala; more precise discrimination, including 64bit option;

less ambitious version that works with Java 1.5;

clarified default_platform;

more detailed platform identification;

isabelle_path: slightly more liberal root pattern;

added isabelle_path; tuned platform_path; tuned comments;

tune File.isabelle_tool signature;

builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);

removed old primrecs

replaced recdefs by funs

tuned abbrevs;

lcm abs lemmas

gcd abs lemmas

NEWS updated

Improved computation of bounds and implemented interval splitting for 'approximation'.

Added new evaluator "approximate"

tuned

merged

added List_Set and Code_Set theories

merged

merged

arbitrary farewell

expand_path: handle parent (..) elements;

more stats;

merged

Streamlined code

merged

Cleaned up GCD

renamed IsabelleProcess to Isabelle_Process; renamed IsabelleSystem to Isabelle_System;

renamed IsabelleSystem to Isabelle_System; added expand_path; tuned comments; tuned;

standard naming conventions for session and theories;

renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);

proper ML interface set_full_types;

Replaced Suc_remove by Suc_eq_plus1

New ATP option: full types

corrected and unified thm names

merged

merged

Datatype.get_all

corrected handling of free variables in arguments

tuned proof

tuned interfaces of datatype module

add_datatypes does not yield particular rules any longer

merged

add_datatype interface yields type names and less rules

non-public representation;

fixed abbrev !! for \<And>;

merged

merged

simplified proof

uniformly capitialized names for subdirectories

renamed ioa to automaton

renamed ioa to automaton

dropped duplicated lemmas, tuned header

NewNumberTheory depends on Algebra

merged

lemma funcset_id by Jeremy Avigad

lemma finite_image_set by Jeremy Avigad

merged

new lemmas

tuned input: require longer symbol prefix; clarified result: no decode yet, single word with several completions;

moved string utilities to completion.scala; tuned;

Completion of symbols and keywords.

more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++; misc tuning;

Added Library/Fraction_Field.thy: The fraction field of any integral domain

merged

fixed name

observe standard theory naming conventions; modernized headers;

end_timing: checked divisions with sane defaults;

eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);

merged

tuned FuncSet

Lexicon: removed unused max_entry;

use results of relevance-filter to determine additional clauses; (needed for minimize to be able to prove the same problems as sledgehammer)

export proof when exporting problemfile

restructured external_prover

corrected comments

adapted to number theory switch