return updated info record after termination proof

proper context for rule_by_tactic;

conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

hgweb style: show author in filelog; full description in annotate hover

proper context for mksimps etc. -- via simpset of the running Simplifier;

read_const: disallow internal names as usual in visible Isar text;

more explicit treatment of context, although not fully localized;

removed some Emacs junk;

merged

make random engine persistent using code_reflect

repaired subtle misunderstanding: statement names are only passed for name resolution

fixed underscore typo

more coherent naming with ML serializer

dropped code_datatype antiquotation

dropped unnecessary ML code

avoid popular infixes

code_reflect: specify module name directly after keyword

NEWS: code_reflect

merged

updated generated file

modernized structure name

use code_reflect

merged

Tuning the quotient examples

clarified signature; simpler implementation in terms of function's tactic interface

return info record (relative to auxiliary context!)

default termination prover as plain tactic

function: sane interface for programmatic use

ML interface uses plain command names, following conventions from typedef

function: better separate Isar integration from actual functionality

merged

export somehow odd mapa explicitly

exported print_tuple

take into account tupled constructors

avoid code_datatype antiquotation

merged

added an example with a free function variable to the Predicate Compile examples

removed local clone in the predicate compiler

improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type

allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;

'write': actually observe the proof structure (like 'let' or 'fix');

adapted ProofContext.infer_type;

ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;

avoid clash with keyword 'write';

allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;

uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);

disabled spurious invocation of (interactive) sledgehammer;

merged

make Mirabelle happy

remove removed option

merge

parentheses around nested cases

merged

add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)

reintroduced short names for HOL->FOL constants; other parts of the code rely on these

save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code

unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)

redo Sledgehammer proofs (and get rid of "neg_clausify")

removed "sorts" option, continued

remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants

insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs

support Vampire definitions of constants as "let" constructs in Isar proofs

tuning

redid the proofs with the latest Sledgehammer; both an exercise and (for a few proofs) a demonstration of the new Isar proof code

remove Nitpick functions that are now implemented in Sledgehammer

added total goal count as argument + message when killing ATPs

make Sledgehammer more friendly if no subgoal is left

polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs

reintroduce missing "gen_all_vars" call

fix types of "fix" variables to help proof reconstruction and aid readability

allow schematic variables in types in terms that are reconstructed by Sledgehammer

in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore

new Isar proof construction code: stringfy axiom names correctly

honor "shrink_proof" Sledgehammer option

remove "higher_order" option from Sledgehammer -- the "smart" default is good enough

updated keywords

exported cert_tyco, read_tyco

added code_reflect command

merged

fix "fors" for proof of monotonicity

merge

merge

Tuned FSet

merged

try to observe intended meaning of add_registration interface more closely

codified comment

merged

empty class specifcations observe default sort

document some known problems with Mac OS;

removed redundant/ignored sort constraint;

tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;

made SML/NJ happy;

updated keywords;

command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;

removed material that is out of scope of this manual;

renamed command 'defaultsort' to 'default_sort';

localized default sort;

more systematic naming of tsig operations;

modernized/simplified Sign.set_defsort;

get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;

export Type.minimize_sort;

term_typ: print styled term

merged

merged

generalize types of path operations

generalize more continuity lemmas

generalized many lemmas about continuity

simplify definition of continuous_on; generalize some lemmas

move intervals section heading

remove unused, redundant constant inv_on

reorganize subsection headings

remove redundant lemma

more lemmas to Vec1.thy

simplify proof

move more lemmas into Vec1.thy

move proof of Fashoda meet theorem into separate file

move definitions and theorems for type real^1 to separate theory file

removed obsolete sanity check -- Sign.certify_sort is stable;

monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;

really minimize sorts after certification -- looks like this is intended here;

tuned signature;

merged

tuned whitespace

got rid of [simplified]

got rid of [simplified]

fix SML/NJ compilation (I hope)

tuned classrel completion -- bypass composition with reflexive edges;

tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;

tuned aritiy completion -- slightly less intermediate data structures;

clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);

misc tuning and simplification;

NEWS and CONTRIBUTORS

explicit is better than implicit

tuned class linordered_field_inverse_zero

merged

instances for *_inverse_zero classes

canonical import

merged

use new classes (linordered_)field_inverse_zero

merged

renamed option

fixes 2a5c6e7b55cb; do not throw out the baby with the bath water

compile

make compile (and not just load dynamically)

merge

introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method; the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure

adapt code to reflect new signature of "neg_clausify"

rename options and keep track of conjecture shape (to facilitate proof reconstruction)

rename options

make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem

remove needless code that was copy-pasted from Quickcheck (where it made sense)

cosmetics

cosmetics

move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"

support readable names even when Isar proof reconstruction is enabled -- useful for debugging

cosmetics: rename internal functions

cosmetics

remove "show_skolems" option and change style of record declarations

remove "skolemize" option from Nitpick, since Skolemization is always useful

removed Nitpick's "uncurry" option

fix typesetting

Fruhjahrsputz: remove three mostly useless Nitpick options

remove type annotations as comments; Nitpick is now 1136 lines shorter

cosmetics

better error reporting; in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs

cosmetics

reuse timestamp function

stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name

make "ATP_Manager.get_prover" a total function, since we always want to show the same error text

remove some bloat

now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script

renamed module "ATP_Wrapper" to "ATP_Systems"

move the minimizer to the Sledgehammer directory

remove debugging code

move some sledgehammer stuff out of "atp_manager.ML"

give an error if no ATP is set

move the Sledgehammer menu options to "sledgehammer_isar.ML"

centralized ATP-specific error handling in "atp_wrapper.ML"

handle ATP proof delimiters in a cleaner, more extensible fashion

merged

fix another if-then-else parse error

fix if-then-else parse error

merged

fix syntax precedence declarations for UNION, INTER, SUP, INF

syntax precedence for If and Let

fix lots of looping simp calls and other warnings

fix duplicate simp rule warnings

define finer-than ordering on net type; move some theorems into Limits.thy

generalize type of continuous_on

define nets directly as filters, instead of as filter bases

use 'example_proof' (invisible);

command 'example_proof' opens an empty proof body;