merged

moved constants inverse and divide to Ring.thy

moved constants inverse and divide to Ring.thy

division ring assumes divide_inverse

rely less on ordered rewriting

merged

merged

merged (manual for "nitpick_hol.ML" and "kodkod.ML")

optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers

make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick

added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability

handle Nitpick's nonstandard model enumeration in a cleaner way; and renumber the atoms so that we get more often a_1 and a_2 and less often a_{n-1} and a_{n-2} in counterexamples

proper quoting of file paths when invoking Kodkodi from Nitpick

merged

optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil"; this gains one cardinality in the AA tree examples in the Nitpick manual

adapted example following previous Nitpick change and fixed minor optimization in Nitpick

split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come

removed obsolete CVS Ids;

modernized translations;

modernized syntax translations, using mostly abbreviation/notation; minor tuning;

simple proofs make life faster and easier

merged

hide fact names clashing with fact names from Group.thy

dropped lemma duplicates

isatest: activated HOL-Nitpick_Examples (by adding component kodkodi) on some platforms where it mostly works as expected;

adjusted to cs. 9f841f20dca6

merged

correct definedness side conditions for copy_apps and take_apps

handle case where copy_stricts cannot be proven; rewrite proof script for take_apps

rewrite proof script for take_stricts

remove redundant theorem attributes

add lemma iterate_below_fix

modernized some syntax translations;

more precise dependencies;

merged

re-generated certificates

renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields

tuned spelling

tuned proofs

hide fact Nat.add_0_right; make add_0_right from Groups priority

tuned header

using code antiquotation

tuned header

dropped accidental duplication of "lin" prefix from cs. 108662d50512

NEWS: ax_simps

avoid upto in generated code (is infix operator in library.ML)

separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4

merged

more precise proofs

moved auxiliary lemmas to more appropriate places

separate library theory for type classes combining lattices with various algebraic structures; more simp rules

dropped instantiations for combined lattices

added lemmas involving Min, Max, uminus

tuned proof

separate library theory for type classes combining lattices with various algebraic structures

more quotes;

merged

separate theory for index structures

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration

split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts, modernized perl scripts: prefer standalone executables

removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);

modernized perl scripts: prefer standalone executables; exec bash wrapper script directly -- avoid intermediate process;

modernized perl scripts: prefer standalone executables;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

prefer explicit @{lemma} over adhoc forward reasoning;

simplified interface for ML antiquotations, struct_name is always "Isabelle";

tuned isatest ML_OPTIONS;

removed ever experimental support for Moscow ML -- hardly works anymore;

result: Single_Assignment.var;

removed slightly adhoc single-assignment feature, cf. structure Single_Assignment; access: uninterruptible update/broadcast, to prevent lost signals;

explicit representation of single-assignment variables;

fixed spelling;

removed unused "boundary" of Table/Graph.get_first;

proper treatment of paths passed to the shell -- to allow spaces in file names as usual;

renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;

misc tuning;

merged

adjusted to changeset 118b41bba42b5

tuned font handling; explicit workaround for Apple's font manager in Java 1.6, which fails to create "IsabelleTextBold" as family member of "IsabelleText";

updated versions of requirements;

filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);

eliminated self intersection and non-integer coordinates;

try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;

updated generated files;

merged

Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"

capture error messages (of SMT solvers)

updated dependencies

merged

updated SMT certificates

updated examples due to changes in the way SMT certificates are stored

merged

merged

Adapted to changes in cases method.

Adapted to changes in setup of cases method.

Added setup for simplification of equality constraints in cases rules.

Added infrastructure for simplifying equality constraints in cases rules.

Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.

updated SMT certificates

updated SMT examples

collect certificates in a single file

added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick

Removed explicit type annotations

adjusted to changes in List_Set.thy

more correspondence lemmas between related operations

canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

dropped some redundancies

generalized lemma foldl_apply_inv to foldl_apply

more correspondence lemmas between related operations; tuned some proofs

new theory Algebras.thy for generic algebraic structures

dropped mk_left_commute; use interpretation of locale abel_semigroup instead

merged

a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML

lemma Image_closed_trancl

corrected type of typecopy constructor

tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

Changed author; removed debugging code.

merged

adding Mutabelle to repository

Replaced vec1 and dest_vec1 by abbreviation.

merged

HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)

merged

support skolem constant for extensional arrays in Z3 proofs

drop underscores at end of names coming from Boogie

merged

correctly hiding facts of Lazy_Sequence

corrected and simplified Spec_Rules registration in the Recdef package

merged

adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps

adopting Sequences

added registration of equational theorems from prim_rec and rec_def to Spec_Rules

merged

function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations

merged

refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck

simplified proofs

NEWS

more accurate dependencies

code literals: distinguish numeral classes by different entries

cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation

merged

dropped some old primrecs and some constdefs

explicit CONST in translations

modernized syntax

fix issues with previous Nitpick change

merged

some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"

removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value

Added transpose_rectangle, when the input list is rectangular.

Add transpose to the List-theory.

some examples for basic context operations;

minimal tuning of this slightly dated material;

added Subgoal.FOCUS; misc tuning and clarification;

misc tuning and clarification;

moved examples to proper place;

more details on long names, binding/naming, name space; tuned;

Variable.names_of; tuned;

more details on Isabelle symbols;

theory data example;

basic setup for ML examples: tag "mlex";

tuned signature;

formal markup of type aliases; updated/tuned/clarified contexts; misc tuning and clarification;

make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);

Netbeans Library "Scala-compiler";

union is an abbreviation for sup.

merged

Eliminated is_open option of Rule_Cases.make_nested/make_common; use Rule_Cases.internalize_params to rename parameters instead.

Adapted to changes in induct method.

Adapted to changes in setup of induct method.

Expand proofs of induct_atomize'/rulify'.

Changed case names of converse_rtranclp_induct.

Injectivity / distinctness theorems are now used to simplify induction rules.

same_append_eq / append_same_eq are now used for simplifying induction rules.

Tuned some proofs; nicer case names for some of the induction / cases rules.

Added setup for simplification of equality constraints in induction rules.

Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.

spurious proof failure

merged

merged

dropped unused binding

dedicated conversions to and from Int

printing of cases

tuned for products vs. tupled functions

added Scala setup

allow individual printing of numerals during code serialization

reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)

adjusted to changes in code equation administration

explicit abstract type of code certificates

corrected error messages; tuned

function transformer preprocessor applies to both code generators

merged

code certificates as integral part of code generation

import of antiquote_setup not necessary

merged

being more accurate wrt. list syntax

deactivate pretty code test for Scala -- no proper setup yet

some syntax setup for Scala

added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;

merged

Parsing errors during proof reconstruction now give rise to an intelligible error message.

rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs; misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;

tuned initial properties/perspective;

provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;

updated version and dependencies;

recovered subscript (cf. ded5b770ec1c);

formal antiquotations for ML snippets; no "open" unsynchronized references

clarified terminology;

merged

added code certificates

tuned code equations

Matrices form a semiring with 0

incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);

ignore some src/Tools/jEdit stuff;

merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b

more timing;

more tobust treatment of Document.current_state; some timing;

new unparsed span for text right after existing command; tuned;

Outer_Lex.is_ignored;

simplified Text_Edit;

eliminated strange mutable var commands; removed_commands: refer to old commands; misc tuning;

updated header;

eliminated obsolete isabelle.proofdocument.Token;

do not override Command.hashCode -- which was inconsistent with eq anyway; unparsed: no id, commands observe pointer equality; actually invoke edit_commands; more correct doc_edits; tuned;

renamed Command.content to source; reorganization of document parsing, using command spans etc. -- initial setup;

further tuning of command_start;

refrain from poking blink rate -- might get stuck in invisible state;

eliminated Command.stop, which tends to case duplicate traversal of commands;

iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;

tuned document changes;

misc tuning and clarification of Document/Change;

adhoc reset of blink rate; bind "console" instance;

provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;

redirect scala.Console output during interpretation; misc tuning;

bind "session"; added printInfoMessage; added stop -- re-inits the interpreter;

export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;

removed unused var plugin;