refer to isabelle.Main application wrapper;

display return code like Isabelle.app on Mac OS;

default Isabelle application wrapper -- JVM entry point for Isabelle.exe;

updated Isabelle.exe specification, assuming layout of bundle;

USER_HOME settings variable points to cross-platform user home directory;

new example theory for quotient/transfer

update NEWS for transfer/quotient

enable variant of transfer method that proves an implication instead of an equivalence

moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator

merged

NEWS for transfer, lifting, and quotient

new example theory for transfer package

some builtin session timing;

move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose

tuned proofs

add transfer rule for List.set

remove duplicate of lemma id_transfer

added covariant relator set_rel, with transfer rules for set operations

renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

tried to make SML/NJ happy

tuned "max_relevant" defaults for SMT solvers based on Judgment Day

prepend PWD to relative paths

reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures

swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations

new transfer package rules and lifting setup for lists

strengthen rule list_all2_induct

more standard Theory_Data setup; keep meta-comments within the history;

merged

add transfer rule for nat_case

uniform naming scheme for transfer rules

rename 'correspondence' method to 'transfer_prover'

hide the invariant constant for relators: invariant_commute infrastracture

improved interleaving of start_execution vs. cancel_execution of the next update;

tuned proofs;

always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

tuned;

simplified internal actor protocol;

builtin timing for main operations;

add secondary transfer rule for universal quantifiers on non-bi-total relations

move definition of set_rel into Library/Quotient_Set.thy

add transfer rule for 'id'

add new transfer rules and setup for lifting package

setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq

NEWS

hide code generation facts in the Float theory, they are only exported for Approximation

merged

forgot to add file

make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules

merged

NEWS

transfer now handles Let

merged

added revised version of Abs_Int

add transfer rule for Let

add code lemmas for word operations

tuned whitespace

dropped dead code

rename no_code to no_abs_code - more appropriate name

use tnames for bound variables in rsp thms

true delayed evaluation of "SPASS_VERSION" environment variable

merged

use latest Z3

merged

reorganised IMP

use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems

use lifting to introduce floating point numbers

replace the float datatype by a type with unique representation

add lemmas to remove real conversions when compared to power of numerals

add simp rules to rewrite comparisons of 1 and real

add lemma to equate floor and div

add powr_inj

add lemmas to rewrite powr to power

add lemmas to compare log with 0 and 1

add ceiling_diff_floor_le_1

display Java 7 only code for now (cf. b9e2ed4b1579);

some sidekick options for more advanced completion;

custom ListCellRenderer with text area font ensures that symbols are displayed reliably;

tuned imports;

more robust wrt. exceptions;

accomodate digits within Isar command names, notably 'try0';

more robust Sledgehammer in Prover IDE;

test with jdk-7u3 that is also bundled;

create thm names correctly

updated components according to tentative bundle;

back to isatest with official polyml-5.4.1 (cf. ffa6e10df091);

use simpler method for preserving bound variable names in transfer tactic

tuned lemmas (v)image_id; removed duplicate of vimage_id

use latest SPASS

doc update

dropped dead code; tuned

generate abs_induct rules for quotient types

tuned

corrected Nbe.static_value: ignore cached compilations; tuned

tuned heading

tuned name

improved threading of thy-values through interpret functions;