Turned Sem into an inductive definition.

Corrected handling of "for" parameters.

induct_true_def and induct_false_def are already contained in induct_rulify_fallback.

added lemma about irreflexivity of pointer inequality in Imperative_HOL

added function ffilter and some lemmas from Finite_Set to the FSet theory

merged

avoid if on rhs of default simp rules

avoid exception Empty on malformed goal

locale predicates of classes carry a mandatory "class" prefix

a ring_div is a ring_1_no_zero_divisors

NEWS

merged

merged

complete_lattice instance for net type

swap ordering on nets, so x <= y means 'x is finer than y'

fixrec no longer uses global simpset internally to prove equations

move setsum lemmas to Product_plus.thy

remove duplicate lemmas

add lemmas about convergent

Cleanup information theory

Moved Convex theory to library.

Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.

proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;

simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result; specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;

UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;

replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;

renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;

minor tuning of Thm.strip_shyps -- no longer pervasive;

simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;

old NEWS on global operations;

ProofContext.init_global;

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

merged

do not generate code per default -- touches file of parent session

made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)

Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)

now if this doesn't make SML/NJ happy, nothing will

more stats;

renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;

slightly more standard induct_simp_add/del attributes; provide explicit context for internal addsimps;

map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

export Simplifier.with_context;

removed some old comments;

merged

merged

generalize lemma adjoint_unique; simplify some proofs

fix latex url

merged

define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general

remove unused function vector_power, unused lemma one_plus_of_nat_neq_0

move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy

remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead

generalize LIMSEQ_vector to tendsto_vector

generalize orthogonal_clauses

remove redundant lemma vector_dist_norm

remove redundant lemma norm_0

generalize some euclidean space lemmas

prove lemma openin_subopen without using choice

move path-related stuff into new theory file

add new Multivariate_Analysis files to IsaMakefile

move operator norm stuff to new theory file

eliminated spurious sledgehammer invocation;

merged

merged

merged

enclose case expression in brackets

catch the right exception

eliminate trivial case splits from Isar proofs

remove debugging code

merged

minor improvements

identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)

added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)

in "overlord" mode: ignore problem prefix specified in the .thy file

uncomment code

redid some Sledgehammer/Metis proofs

fix more "undeclared symbol" errors related to SPASS's DFG format

be more discriminate: some one-line Isar proofs are silly

one-step Isar proofs are not always pointless

the SPASS output syntax is more general than I thought -- such a pity that there's no documentation

redo more Metis/Sledgehammer example

fixed definition of "bad frees" so that it actually works

don't remove last line of proof

handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction

make SML/NJ happy, take 2

use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)

expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute

more neg_clausify proofs that get replaced by direct proofs

redo some of the metis proofs

back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs

improve unskolemization

make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point

properly extract SPASS proof

try out Vampire 11 and parse its output correctly; will revert to Vampire 9 if 11 doesn't perform as well

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';