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

more data structure refactoring

data structure rationalization

tuning

refactored preplaying outcome data structure

distinguish not preplayed & timed out

pick up tfree/tvar type from SPASS-Pirate proof

tuning

extended ATP types with sorts

removed debugging output

honor SPASS-Pirate type arguments

made SML/NJ-friendlier (hopefully)

made timeouts in Sledgehammer not be 'option's -- simplified lots of code

simplified data structure

prevent curl's output to interfere with the prover's output

tuning

merge

parse SPASS-Pirate types

merged

added lemma

merge

pass down user input in more cases in order to preserve "let"s etc.

pass auto-proved exhaustiveness properties to tactic; rightly use "%_. False" instead of undefined for unspecified conditions; get rid of ugly "if True then ... else Code.abort" in auto-generated code equations;

merge

changed pirate port

fixed variable confusion introduced by 'tuning' change 565f9af86d67

made SML/NJ happier

try 'auto' first -- more likely to succeed

new port

tuning

generate type classes for tfrees

modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

avoid clashes of fact names

initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

reduced cardinals dependencies of (co)datatypes

tighter bnf bounds for (co)datatypes

tuned

tuning