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