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;