renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax; removed redundant lemma UU_least

merged

updated SMT certificates

re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs

tuned whitespace

do not open structure Codegen;

do not open auxiliary ML structures;

uniform treatment of type vs. term environment (cf. b654fa27fbc4); tuned;

uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);

tuned isatest settings;

merged

more robust decomposition of simultaneous goals

function (default) is legacy feature

more scalable Symbol_Pos.explode;

tuned ML toplevel pp for type string: observe depth limit;

theory loader: implicit load path is considered legacy;

explicit file specifications -- avoid secondary load path;

check_file: secondary load path is legacy feature;

share_common_data dummy;

made SML/NJ happy;

made SML/NJ happy;

tuned comments;

made SML/NJ happy; more accurate dependencies;

made SML/NJ happy;

function (tailrec) is a legacy feature

dropped duplicate unused lemmas; spelling

partial_function (tailrec) replaces function (tailrec); dropped unnecessary domain reasoning; curried polydivide_aux

remove lemma ideal_completion.principal_induct2, use principal_induct twice instead

NEWS updates for HOLCF

replaced separate lemmas seq{1,2,3} with seq_simps

changed syntax of powerdomain binary union operators

tuned order of NEWS

NEWS

documentation stub on type_lifting

tuned comments and line breaks

rename function ideal_completion.basis_fun to ideal_completion.extension

fix another proof script broken by a35af5180c01

fix proof script broken by a35af5180c01

merged

full localization with possibly multiple entries; explicit prohibition of fixed type variables

tool-compliant mapper declaration

more proof contexts; formal declaration

mapper is arbitrary term, not only constant; proper backward proofs of derived properties

tuned comment

merged

made SML/NJ happy

check JVM later, to avoid potential conflict with jEdit splash screen;

explicit JVM check on startup;

more explicit jvm_name;

isabelle java: prefer -server here;

configuration option "rule_trace"; discontinued preference "trace-rules";

configuration option "syntax_branching_level";

configuration option "syntax_ast_trace" and "syntax_ast_stat";

more robust ML antiquotations -- allow original tokens without adjacent whitespace;

configuration option "ML_trace";

merged

id_const replaces mk_id

tuned type_lifting declarations

prove more algebraic version of functorial properties; retain old properties for convenience

declare more simp rules, rewrite proofs in Isar-style

merged

use DERIV_intros

generalized monoseq, decseq and incseq; simplified proof for seq_monosub

merged

proper static closures

tuned names

renamed mk_id to the more canonical id_const

merged

better parsing of options, in case the value has '='

show the relation

merged

renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy"

added "sledgehammer_tac" as possible reconstructor in Mirabelle

merged

merged

also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)

Enabled non fully polymorphic map functions in subtyping

make SML/NJ and Poly/ML agree on the type of "before";

only depend on exisiting statements

merged

evaluator separating static and dynamic operations

tuned naming

evaluator separating static and dynamic operations

canonical handling of theory context argument

merged

evaluator separating static and dynamic operations

program is separate argument to serializer

more explicit structure for serializer invocation

merged

tuned proof

HOLogic.mk_id

avoid weird symbols in path

mechanism to keep SMT input and output files around in Mirabelle

proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction

added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)

enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day

Cygwin: Poly/ML 5.4.0 requires libgmp3;

updated to polyml-5.4.0;

tuned;

updated for Poly/ML 5.4.0;

merged

avoid ML structure aliases (especially single-letter abbreviations)

added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions

merged

configure domain package to work with HOL option type

make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction

simplify proofs

beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction

configure domain package to work with HOL sum type

replace list_map function with an abbreviation

merged

run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy

disable feature that was enabled by mistake

make exceptions more transparent in "debug" mode

remove spurious line

use the options provided by Stephan Schulz -- much better

optionally supply constant weights to E -- turned off by default until properly parameterized

merged

type_lifting for predicates

proper identifiers for consts and types;