tuned whitespace

tuned proof

tuned proof

distributed lattice properties of predicates to places of instantiation

removing some unnecessary premises from Divides

simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)

observe HEIGHT of overview ticks; misc tuning and clarification;

more careful painting of overview component: more precise and more efficient;

clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;

use qualified constant names instead of suffixes (from Florian Haftmann)

tuned proofs

tuned

brute-force adjustion

tuned whitespace

tuned

tuned

tuned code

dropped whitespace

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

corrected typo

dropped dead code

notepad is more appropriate here

corrected treatment of applications of built-in functions to higher-order terms

NEWS

merged

added congruence rules for Option.{map|bind}

updated generated documents

avoid redefinition of @{theory} antiquotation

update of generated documents

tuned whitespace

clarified

corrected spelling

clarified

more precise semantics of "theory" antiquotation

tuned import

dropped references to obsolete theories

adjusted to set type constructor

tuned whitespace

more explicit error on malformed abstract equation; dropped dead code; tuned signature

simplified configuration options for syntax ambiguity;

retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);

more antiquotations;

more symbols; misc tuning;

tuned imports;

tuned proofs;

simplified configuration options for syntax ambiguity;

merged

removing unnecessary premise from diff_single_insert

explicit is better than implicit;

more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);

simplifying proof

removing unnecessary premises in theorems of List theory

tuning mutabelle script

adding documentation for abort_potential option in quickcheck

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);

uniform Isar source formatting for this file;

clarified outer syntax "constdecl", which is only local to some rail diagrams;

discontinued obsolete "prems" fact;

eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);

removed obsolete files;

more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);

removed dead code;

updated listrel (cf. 80dccedd6c14);

removed redundant cut_inst_tac -- already covered in implementation manual;

updated rewrite_goals_rule, rewrite_rule;

NEWS;

updated refs;

renamed "xstr" to "str_token";

merged

don't report spurious LEO-II errors

better error message

removing debug code in mutabelle

adding abort_potential functionality in quickcheck

adding abort_potential configuration in Quickcheck

clarified bires_inst_tac: retain internal exceptions;

tuned signature;

more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;

more conventional tactic setup;

eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);

prefer high-level elim_format;

discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;

method setup;

simplified use of tacticals;

comment;

tuned signature, according to actual usage of these operations;

tuned signature;

normalized aliases;

elininated unused INTLEAVE;

eliminated unused rewrite_goal_rule;

eliminated unused subgoals_tac;

eliminated obsolete aliases;

eliminated obsolete aliases;

tuned;

merged, resolving trivial conflicts;

merged;

new SPASS options

making num_mutations a configuration that can be changed with the mutabelle bash command

making max_mutants an option that can be changed in the Mutabelle-script

increase timeout to 30 seconds; changing mutabelle script

parse clauses generated from several formulas

be more gentle when generating KBO weights

update SPASS slices

more specification of the quotient package in IsarRef

specification of the quotient package

tune KBO weight code

minor DFG fix