farewell to theory More_List

dropped unused nth_map

more explicit NEWS

refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";

tuned;

improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;

tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);

recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);

more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);

proper refs;

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes

prefer listsum over foldl plus 0

prefer concat over foldl append []

tuned proofs

interaction of set operations for execution and membership predicate

cleanup of code declarations

discontinued Syntax.positions -- atomic parse trees are always annotated;

improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;

misc tuning;

prefer raw_message for protocol implementation;

prefer raw_message for protocol implementation; tuned;

prefer raw_message for protocol implementation;

tuned signature;

tuned signature -- emphasize special nature of protocol commands;

updated version information;

updated version information; discontinued somewhat obsolete hotspot check: OpenJDK 1.7 works reasonably well, and final bundling provides certain tested JDK/JRE versions;

generalised type

improved "set" support by code inspection

remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder

tuning

handle higher-order occurrences of sets gracefully in model display

prefer explicit version information;

more Nitpick doc updates

reenable Kodkodi in Mira now that Nitpick has been ported to 'a set constructor

reenable Kodkodi in Isatest now that Nitpick has been ported to 'a set constructor

fixed bisimilarity axiom -- avoid "insert" with wrong type

tuning

updated Nitpick docs after "set" reintroduction

no abuse of notation

always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)

more robust destruction of "set Collect" idiom

handle starred predicates correctly w.r.t. "set"

handle "Id" gracefully w.r.t. "set"

reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature

handle "set" correctly in Refute -- inspired by old code from Isabelle2007

create consts with proper "set" types

tuned Refute

lower cardinality for faster testing

simplify mem Collect

tuning

ported Minipick to "set"

fixed set extensionality code

tuned import

construct correct "set" type for wf goal

fixed Nitpick's typedef handling w.r.t. "set"

fixed type annotations

rationalized output (a bit)

fixed a few more bugs in \Nitpick's new "set" support

regenerate SMT example certificates, to reflect "set" type constructor

port part of Nitpick to "set" type constructor

reintroduced failing examples now that they work again, after reintroduction of "set"

ported mono calculus to handle "set" type constructors

fixed spurious catch-all patterns

more benchmarks; tuned;

tuned

ported "Sets" example to "set" type constructor

ported a dozen of proofs to the "set" type constructor

reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow

update docs to reflect "Manual_Nits"

removed special handling for set constants in relevance filter

reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

killed unfold_set_const option that makes no sense now that set is a type constructor again

tuned

removed unnecessary lemmas

tuned proofs

tuned var names

tuned argument order

merged

add simp rules for bitwise word operations with 1

tuned types

disabled failing sledgehammer unit test (collateral damage of 184d36538e51)

disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)

merged

Made gen_dest_case more robust against eta contraction

merged

remove unnecessary intermediate lemmas

tuned;

eliminated old-fashioned Global_Theory.add_thms;

simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;

simplified proof;

simplified proof;

simplified proof;

more parallelism;

tuned;

merged

tuned -- afford slightly larger simpset in simp_defs_tac;

tuned -- standard proofs by default;

do not fork skipped proofs;

clarified timeit_msg;

tuned;

comments;

remove constant 'ccpo.lub', re-use constant 'Sup' instead

merged

tuned

conversions from sets to predicates and vice versa; extensionality on predicates

added implementation of pred_of_set

fundamental theorems on Set.bind

updated generated files;

qualified Finite_Set.fold

qualified Finite_Set.fold

dropped redundant setup

tuned declaration

attribute code_abbrev superseedes code_unfold_post; tuned text

attribute code_abbrev superseedes code_unfold_post; tuned names and spacing

attribute code_abbrev superseedes code_unfold_post

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

merged

merged