comment

nicer output

rationalized output

generate Meng--Paulson facts for evaluation purposes

tuning

export useful functions

instantiate induction rules

MaSh evaluation driver

moved MaSh into own files

distinguish updates and queries + cleanups

don't ask E to generate a detailed proofs if not needed

tuning

gracefully compute cardinality of sets (to avoid type protectors)

better tautology elimination

generate lambdas and skolems again

tuning

generate deep terms as feature

generate theory name as a feature

adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)

merged

adding the hotel key card example in Quickcheck-Examples

adding a missing entry to predicate compiler's setup

compile

tuning

cleanup

more precise dependencies -- eliminate tautologies

generate problem file

improve feature list generation

cleaner accessibility file

first go at generating files for MaSh (machine-learning Sledgehammer)

abandoned import of isatest reports into (old version of) mira -- unstable, and not worth the maintenance effort

make sure var/running dir exists for isatest

removed switched-off atbroy102 from isatest; no cygwin test currently running, needs a working server somewhere

prefer lxbroy[23] as standard test machines;

discontinued XSYMBOL_INSTALLFONTS (cf. 40fab092d2a2);

discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);

tuned;

discontinued obsolete attribute "COMP";

merged

make SML/NJ happy + tuning

tune type arg handling

tuning

fiddled with "tags_at" a bit -- the only non-tuning part of the change is a slight simplification of the typing axioms

remove needless type arguments to "tags_at" encoding

removed obsolete psbooklet;

more directory structure;

explicit is better than implicit;

removed obsolete rev_contrapos (cf. 1d195de59497);

tuned proofs -- eliminated old-fashioned COMP and rev_contrapos;

prefer sys.env from scala 2.9;

prefer sys.exit from scala 2.9;

internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;

more explicit directory structure Admin/Release/; updated to Admin/components;

merged

Stub theory for division on functionals.

slightly modernized ISABELLE_GHC etc. -- /usr/bin is more likely to provide it by default (notably on macbroy2[0-9] and lxbroy*);

more precise cover

don't generate any type class axioms for free types for monomorphic encodings

update docs

tuning

prefer hook in Admin/ to initialize components

corrected: avoid shadowing of variable

merged

adding some minimal documentation and an example of quickcheck's interfaces

exporting important function for the "many conjecture refutation" compilation of quickcheck

merged

new type class for computing finiteness of types with instantiations

add finiteness lemmas for 'a * 'b and 'a set

adding a challenging example in the examples file

eta-expanded occurences of algebraic functionals are simplified by default

not all Linuxen understand -Ssmpt= and defaults seem to be configured correctly now

default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);

removed generated stuff to avoid bit rot;

merged

Documented "incomplete" option of spark_end

Various improvements - show names of remaining VCs after spark_open and spark_vc - spark_status now also shows names of conclusions - spark_end now also accepts pending VCs, if "incomplete" option is given - VCs whose proofs contain oracles are no longer declared as proved in the corresponding *.prv file

no ml-platform-specific components

instantiate card_UNIV with nibble and code_numeral

change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code

add generic phantom type

added universal jdk-6u31 as standard component;

added ProofGeneral-4.1 as standard component, which allows to discontinue special choosefrom magic eventually;

merged

adding a useful remark in the reference

more tests on lxbroy[234], which are 4 core Xeon machines;

moved crontab to lxbroy2, one of the newer server machines; avoid macbroy27 for now due to spurious NFS issues;

some files for universal JDK 1.6.0_31 component;

corrected name of components file

prefer stderr for warnings

include jedut_build among canonical components

support for platform-specific components

correction: proper initialization of existing component

snippet to be sourced in user settings file in order to initialize components for a repository revision; the initialization is »liberal« since there is no obvious solution yet for components whose distribution is restricted

more standard filename for common components

updated crontab on macbroy27 and macbroy2;

use macbroy27 instead of macbroy28, which is broken for several weeks already;

reintroduced "t@" encoding, this time sound

compile

tuning

renamed experimental option

finished implementation of DFG type class output

more work on DFG type classes

more work on class support

generate type classes for polymorphic DFG format (SPASS)

avoid detour through terms

cleanly distinguish between type declarations and symbol declarations

removed old hack now that types and terms are cleanly distinguished in the data structure

added sorts to datastructure

robustness -- TFF1 does not support type classes

implement polymorphic DFG output, without type classes for now

added type arguments to "ATerm" constructor -- but don't use them yet

started adding polymophic SPASS output

tuning

removed support for unsorted DFG, now that SPASS 3.7 is no longer supported

merged, resolving conflict with 87c831e30f0a;

eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;

prefer direct rotate_prems over old-style COMP;

tuned proofs -- prefer direct "rotated" instead of old-style COMP;

ignore morphism more explicitly; tuned headers;

some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing