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