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