exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler

added diagnostic printing; changed proof for parameters; moved code

merged

simplified binding concept

temporary workaround

tuned

streamlined code

dropped id

mutual instances

canonical prefix for datatype derivates

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