killed obsolete provers from documentation

merged

removed obsolete remote_cvc3 and remote_z3

implicit "cartouche" method (experimental, undocumented);

more examples;

cartouche within antiquotation;

cartouche within nested args (attributes, methods, etc.);

group symbols;

prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers

table for code symbols

HTML output for \<newline>;

sorted entries according to components_checksum;

more unicode tokens; diff -r ProofGeneral-4.2/isar/isar-unicode-tokens.el ProofGeneral-4.2-1/isar/isar-unicode-tokens.el 356c356,359 < ("some" "ϵ")) --- > ("some" "ϵ") > ("open" "‹") > ("close" "›") > ("newline" "⏎"))

prefer Isar commands over old-fashioned ML (see also a189c6274c7a); removed pointless space: the second "_ \<Colon> _" should take precendence anyway;

crude latex macro for \<newline;

proper \<newline>;

unused;

tuned;

support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;

back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;

tuned;

prefer user-space tool within Pure.thy;

clarified @{rail} syntax: prefer explicit \<newline> symbol;

clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);

folded 'Wellfounded_More_FP' into 'Wellfounded'

folded 'Order_Relation_More_FP' into 'Order_Relation'

support declaration of nonemptiness witnesses in bnf_decl

hide short const name

get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'

liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts

compile (importing 'Metis' or 'Main' would have been an alternative)

dissolved 'Fun_More_FP' (a BNF dependency)

moved lemmas from 'Fun_More_FP' to where they belong

moved 'Zorn' into 'Main', since it's a BNF dependency

adapted to move of Wfrec

moved Wfrec to Main, since it is a dependency of cardinals, hence BNFs

added \<newline> symbol, which is used for char/string literals in HOL;

general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);

merged

fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;

tuned text

tuned

automatically solve proof obligations produced for code equations

use 'disc_exhausts' property both from types on which 'case's take place and on return type

activation of Z3 via "z3_non_commercial" system option (without requiring restart);

tuned;

use the right context in 'unfold_thms id_def'

repaired 'ctr' tactic w.r.t. 'split'

tuned

merged

NEWS;

proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;

clarified context;

tuned signature; clarified context;

tuned signature;

check_hyps when attributes are applied;

more accurate context;

reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);

check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;

clarified context;

clarified context;

tuned signature;

shot in the dark to make LaTeX happy again

provide default name in splitted representation

dropped legacy alias feature

merged

disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');

more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;

more accurate context;

tuned;

explicit check of background theory;

basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)

correctly extract code RHS, with loose bound variables

cope gracefully with missing ctr equations by plugging in 'False ==> ...'

strengthened tactic to handle 'disc_iff' equations of the form '... = False'

repair 'exhaustive' feature for one-constructor types

pass right rhs as code rhs

use correct default for exclude rules to avoid weird tactic failures

tuning (no need for |-> here)

fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')

tuning

only destruct cases equipped with the right stuff (in particular, 'sel_split')

generate 'disc_iff' for all discriminators

use 'disc_iff' as simp rules whenever possible + clean up '= True', '= False', etc.

exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial

merged

more robust;

merged

tuned;

access X11 window manager;

new codatatype example: stream processors

use the right context in tactic

fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments

do not use wrong constructor in auto-generated proof goal

fixed de Bruijn bug in 'unfold_lets'

tuned error message

reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes

strengthened tactics w.r.t. 'lets' and tuples

strengthen tac w.r.t. lets with tuples

use 'prove_sorry'

for code equations that coincide with ctr equations, make sure the usr's input is preserved for both

made 'datatype_new_compat' work with sort constraints

merge

match order of generated theorems to user input; improve exhaustiveness criterion to prevent exception

typo

ensure that schematic type variables are fresh in rty

ensure that the raw type of an abstract type cannot be treated as an abstract type recursively

tuned

avoid hard tabs in output -- somewhat ill-defined;

uniform output of tracing via official channel (usually depending on trace flag); warning subject to context visibility;

tuned

merged

more informative error message;

obsolete / unmaintained;

misc tuning and clarification;

more formal ISABELLE_BROWSER_INFO;

tuned comments;

dropped legacy

order and graph for code symbols

special treatment of ==> and == solely as constants

uniform orientation of instances as (type constructor, type class)

minimized class dependency, updated references

proper context for simplifier invocations in code generation stack

spelling

proper name generation to avoid clash with 'P' in user specification

more SML-ish (less Haskell-ish) naming convention

strengthened tactic

refactoring

instantiate schematics as projections to avoid HOU trouble

tuning

avoid schematic variable in goal, which sometimes gets instantiated by tactic

generalized tactic to the case of several assumptions per equation

made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)

made tactic more robust

made tactic handle corner cases, where some of the 'disc' properties are missing, correctly

simplified code

prevent tactic from getting out of sync and wrongly attack next subgoal

removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)

consider code as exhaustive

proper handling of corner case, take 2

robustness

properly synchronize parallel lists

graceful handling of one-constructor case

gracefully handle single-equation case, where 'nchotomy' is 'True'

made tactic handle gracefully the case of missing constructors

removed 'nchotomy' property

don't generate any proof obligation for implicit (de facto) exclusiveness

detect syntactic exhaustiveness

internally allow different values for 'exhaustive' for different constructors

internally allow different values for 'sequential' for different constructors

use same name for feature internally as in user interface, to facilitate grepping

generate 'disc_iff' property in 'primcorec'

added tactic to prove 'disc_iff' properties in 'primcorec'

merged

clarified blast after change of SELECT_GOAL in 210bca64b894: do not smash flex-flex pairs of overall goal state (in analogy to maxidx) -- NB: Isar goal structure serves as natural boundary, e.g. in "by blast";

updated keywords;

clarified simplifier context; eliminated Simplifier.global_context;

simplified settings for src/HOL/Tools/SMT;

avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);

dropped obsolete references to recdef

examples how to avoid the "code, code del" antipattern

fundamental treatment of undefined vs. universally partial replaces code_abort

explicit distinction between empty code equations and no code equations, including convenient declaration attributes

tuned whitespace

more precise wording

uniform bookkeeping also in the case of deletion

more abstract declaration of code attributes

dropped unused material

proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;

made SML/NJ happy;

added system option "jedit_print_mode";

avoid hardwired /bin/bash (like canonical Isabelle shell scripts);

tuned whitespace;

simplified

more compact representation of different situations for interpretation

more succint formulation of special case

tuned whitespace

move instantiation here from AFP/Native_Word

dropped junk

postpone dis"useful" lemmas

cleanup

prefix disambiguation

tuned proofs and declarations

prefer target-style syntaxx for sublocale

prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm

self-contained formulation of subclass command, avoiding hard-wired Named_Target.init

ephemeral interpretation also formally works on theory level

abolished slightly odd global lattice interpretation for min/max

prefer more canonical names for lemmas on min/max

explicit distributivity facts on min/max

postponed min/max lemmas until abstract lattice is available

tuned structure of min/max lemmas

prefer abstract simp rule

more lemmas on abstract lattices

tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs

more general induction rule; tuned proofs

convenient printing of polynomial values

prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.

prefer Y_of_X over X_to_Y; prefer alist over assoc_list; prefer explicit prefix

merge

prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)

NEWS

dropped redundant lemma

syntactically tuned

prefer plain bool over dedicated type for binary digits

tuned

compile + reduce problem size by a notch

generate exhaust from nchotomy

made tactic work with theorems with multiple assumptions

renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)

express weak pullback property of bnfs only in terms of the relator

merged

tuned

reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

tuning whitespace

recognize datatype reasoning in SPASS-Pirate

note manually proved exclusiveness property

note exhaust proof obligation

compile

implemented 'exhaustive' option in tactic

tuning

tuning

tuning 'case' expressions

don't do 'isar_try0' if preplaying is off