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

restate some lemmas to respect int/bin distinction

simplify some proofs

add lemma word_eq_iff

restate lemma word_1_no in terms of Numeral1

remove recursion combinator bin_rec; define AND for type int directly with function package

simplify definition of XOR for type int; reorder some lemmas

simplify definition of OR for type int; reorder some lemmas

simplify definition of NOT for type int

add several new tests, most of which don't work yet

fix typos

remove some duplicate lemmas

simplify proof

replace 'lemmas' with explicit 'lemma'

add section headings

remove duplicate lemma lists

reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;

disable kodkodi for now to prevent isatest failure of HOL-Nitpick_Examples due to 'a set constructor; prefer explicit version information;

updated platform information;

discontinued broken macbroy5 and thus the obsolete ppc-darwin platform;

more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;

print case syntax depending on "show_cases" configuration option;

merged

redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min

remove some uses of Int.succ and Int.pred

removed unused lemmas

remove redundant syntax declaration

use 'induct arbitrary' instead of 'rule_format' attribute

declare simp rules immediately, instead of using 'declare' commands

declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin

be explicit about Finite_Set.fold

dropped fact whose names clash with corresponding facts on canonical fold

prefer canonical fold on lists

be explicit about Finite_Set.fold

incorporated More_Set and More_List into the Main body -- to be consolidated later

moved theorem requiring multisets from More_List to Multiset

NEWS: unavoidable fact renames

dropped disfruitful `constant signatures`

moved various set operations to theory Set (resp. Product_Type)

dropped Executable_Set wrapper theory

updated certificate

NEWS: `set` is now a proper type constructor

dropped references to obsolete facts `mem_def` and `Collect_def`

dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`

adjusted to set/pred distinction by means of type constructor `set`

treatment of type constructor `set`

executable intervals

`set` is now a proper type constructor

tuned layout

reduced to a compatibility layer

added setup for executable code

moved `sublists` to theory Enum

commented out examples which choke on strict set/pred distinction

explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`

adjusted to set/pred distinction by means of type constructor `set`

dropped references to obsolete fact `mem_def`

dropped obsolete lemma member_set

dropped obsolete code equation for Id

tuned proofs

generalized type signature to permit overloading on `set`

added monad instance for `set`

enum type class instance for `set`; dropped misfitting code lemma for trancl

finite type class instance for `set`

treatment of type constructor `set`

lattice type class instances for `set`; added code lemma for Set.bind

`set` is now a proper type constructor; added operation for set monad

simplify some proofs

remove redundant lemma word_sub_def

add lemmas bin_cat_zero and bin_split_zero

more uses of 'induct arbitrary'

use 'induct arbitrary' instead of universal quantifiers

remove two conflicting simp rules for 'number_of (number_of _)' pattern

add lemma bin_nth_minus1

removed killed encoding from example

updated docs

killed "guard@?" encodings -- they were found to be unsound

extend previous optimizations to guard-based encodings

treat polymorphic constructors specially in @? encodings

tuning

no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")

added some basic documentation about method induction_schema extracted from old NEWS

adding documentation about the quickcheck_generator command in the IsarRef

extending quickcheck example

NEWS

quickcheck_generator command also creates random generators

don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers

one more SPASS identifier

tuning

merged

meaningful error message on failing merges of coercion tables

add simp rules for enat and ereal

add lemmas

add lemmas

weaken preconditions on lemmas

add lemmas

removing some debug output in quotient_definition

adding quickcheck generators in some HOL-Library theories

adding quickcheck generator for distinct lists; adding examples

added keywords

quickcheck generators for abstract types; tuned

exporting instantiation functions in quickcheck for their usage in abstract generators

generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;

tuned

tuned

ensure TPTP FOF/TFF/THF formulas are close

tuned

merged

added old chestnut

isarfied proof; add log to DERIV_intros

tendsto lemmas for ln and powr

tuned settings;

updated jedit_build component;

updated version information;

patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);

eliminated Drule.export_without_context which is not really required here;

tuned signature;

enforce short hostname on all platforms (especially macbroy2);

clarified modules that contribute to datatype package;

tuned signature;

merged

merged

improved indexed complete lattice

more elementary defs;

eliminated old-fashioned Global_Theory.add_thms(s);

prefer sorting from Scala library;

prefer Name.context operations;

tuned;

clarified modules that contribute to datatype package;

tuned signature;

merged;

tuned;

add complementary lemmas for {min,max}_least

add lemmas about limits

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

separate rep_datatype.ML; tuned signature;

misc tuning and simplification;

more stats;

made SML/NJ happier

merged

tuned

hiding the precious name map_entry in AList_Impl

killed dead code

use new redirection algorithm in Sledgehammer

fixed parsing of TPTP atoms

tuned signature;

avoid fragile Sign.intern_const -- pass internal names directly; tuned;

tuned;

added new proof redirection code

SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite

make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)

NEWS

correcting dependencies after renaming

tuned header after renaming

moving AList theory to AList_Impl to make space for the association lists with invariant

merged

adding map_entry to AList theory

adding map_default to AList theory

fixed typo in theorem name in AList theory

adding code attribute to enable evaluation of equality on multisets

merged

updated Sledgehammer/SMT docs

tuned signature;

eliminated dead code;

some full isatest runs, which include benchmark targets;

more visible benchmarks; uniform IsaMakefile target "full" to cover such extra sessions;

fixed Nitpick definition of "<" on "real"s

replace 'lemmas' with 'lemma'

merged

more simp rules for sbintrunc

add simp rules for sbintrunc applied to numerals

replace many uses of 'lemmas' with explicit 'lemma'

add lemma bin_nth_zero

add simp rules for bintrunc applied to numerals

add simp rules for bin_rest and bin_last applied to numerals

add simp rules for bin_sign applied to numerals

add simp rules for BIT applied to numerals

declare BIT_eq_iff [iff]; remove unneeded lemmas

towards removing BIT_simps from the simpset

type signature for bin_sign

remove some unwanted numeral-representation-specific simp rules

remove redundant lemmas

reorder some definitions and proofs, in preparation for new numeral representation

merged

added lemmas

added concrete syntax

'datatype' specifications allow explicit sort constraints; tuned signatures;

do not open ML structures;

tuned;

removed dead code;

comment;

connect while_option with lfp

lemmas about Kleene iteration

merged

avoid multiple type decls in TFF (improves on cef82dc1462d)

added missing quantifier

remove needless declaration in TFF1 problems

correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i

modernized specifications;

support phantom types as quotient types

merged

merged

tuned

datatype dtyp with explicit sort information; tuned messages;

tuned;

updated generated file;

tuned quickcheck's response

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

merged

replace more uses of 'lemmas' with explicit 'lemma'; replace uses of 'simplified' attribute with 'unfolded'; remove unused intermediate lemmas.

Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.

fix spelling

fix spelling

added IMP/Live_True.thy

replace many uses of 'lemmas' with 'lemma'; remove many unused intermediate lemmas.

prove class instances without extra lemmas

finite class instance for word type; remove unused lemmas

remove unused lemmas

generalize some lemmas

merged

tidied Word.thy; put attributes directly on lemmas instead of using 'declare'; replace various 'lemmas' commands with ordinary 'lemma'.

remove redundant lemma word_diff_minus

remove some duplicate lemmas, simplify some proofs

Quotient_Info stores only relation maps

hiding definitional facts in Quickcheck; introducing catch_match more honestly

added dependencies

added an example file with lifting of constants with contravariant and co/contravariant types

merged

make ctxt the first parameter

context/theory parametres tuned

maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types

add induction rule for list_all2

deactivating quickcheck_narrowing if Efficient_Nat theory is loaded

tuned quickcheck's response

more systematic lemma name

adding examples for quickcheck narrowing about partial functions

removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions

HOLCF/ex/Letrec.thy: keep class 'domain' as default sort

more error checking for fixrec

reinstate old functions cfst and csnd as abbreviations

merged

tuned

merged

added a specific tactic and method that deal with partial equivalence relations

use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts

avoid multiple TFF1 declarations

updated TFF1 support

updated Metis to 20110926 version

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead

add cancellation simprocs for type enat

tuned

increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure

tuned proofs

added lemmas

tuned proof

real is better supported than real_of_nat, use it in the nat => ereal coercion

merged

the note about morphisms moved in the description part

updating documentation about quiet and verbose options in quickcheck

making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples

adding verbose configuration to quickcheck

random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument

the reporting random testing also returns if the counterexample is genuine or potentially spurious

exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly

inverted flag potential to genuine_only in the quickcheck narrowing Haskell code

NEWS

documenting the genuine_only option in quickcheck;

renaming potential flag to genuine_only flag with an inverse semantics

quickcheck narrowing continues searching after found a potentially spurious counterexample

outputing the potentially spurious counterexample and continue search

dynamic genuine_flag in compilation of random and exhaustive

indicating where the restart should occur; making safe_if dynamic

merged

enforce parantheses around SKIP {_}

adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

merged

remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality

missing dependency

improved var names

invariant holds before loop

caret_range based on BreakIterator, which handles combined unicode characters as well;

misc tuning;

some localization;

eliminated some legacy operations;

more antiquotations;

tuned whitespace;

eliminated some legacy operations;

removed dead code, which has never been active in recorded history;

do not open ML structures;

tuned signature;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

adapting exhaustive generators in record package

outputing if counterexample is potentially spurious or not

making catch_match polymorphic

compilations return genuine flag to quickcheck framework

extending quickcheck's result by the genuine flag

reporting random compilation also catches match exceptions internally

the narrowing also indicates if counterexample is potentially spurious

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not

changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier

quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception

adding examples for quickcheck-random

removing exception handling now that is caught at some other point; tuned message

quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;

merged

merged IMP/Util into IMP/Vars

use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure

cardinality of sets of lists

do not import examples Probability theory

moved theorems about distribution to the definition; removed oopsed-lemma

rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

remove duplicate theorem setsum_real_distribution

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

updated Sledgehammer docs with new/renamed options

added "minimize" option for more control over automatic minimization

renamed "slicing" to "slice"

tuning

minor example tweak

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

updated markup conforming to ML side;

discontinued obsolete datatype "alt_names";

misc tuning;

merged

removed outdated comment moved back and updated (at the direct request of Christian Urban)

more stable introduction of the internally used unknown term

prefer typedef without alternative name;

prefer cpodef without extra definition;

prefer typedef without extra definition and alternative name; tuned proofs;

tuned layout;

tuned header;

updated version information;

removed outdated comment

adding examples for the potential counterexamples in the simple scheme

also potential counterexamples in the simple exhaustive testing in quickcheck