tuned;

more accurate class constraints on cancellation simproc patterns

tuned;

tuned Named_Thms: proper binding;

refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

slightly more explicit/syntactic modelling of morphisms;

correct import path

allow to build Probability and MV-Analysis with one ROOT.ML

removing dead code

ex/Simproc_Tests.thy: remove duplicate simprocs

use simproc_setup for cancellation simprocs, to get proper name bindings

tuned;

eliminated aliases of standard functions;

more standard attribute setup;

localized quotient data;

simplified/standardized signatures;

tuned signature;

uses IMP and hence requires its tex setup

merged

tuned text

respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

merged

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

more robust ML pretty printing (cf. b6c527c64789);

tuned;

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

tuned text

tuned names to avoid shadowing

merge Gcd/GCD and Lcm/LCM

clarify types of terms: use proper set type

instance bool :: linorder

removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

fixed typo

latex output not needed because errors manifest themselves earlier

some text on inner-syntax;

renamed in ASM

tuned order of eqns

tuned

script for exporting filtered IMP files as tar.gz

removed Norbert's email from isatest (bounces)

class Lexicon as abstract datatype;

more private stuff;

class Text.Edit as abstract datatype;

class Time as abstract datatype;

class Volatile as abstract datatype;

merged

added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file

experimental support for Scala 2.9.1.final;

class Path as abstract datatype;

class Counter as abstract datatype;

discontinued redundant ASCII syntax;

modernized specifications;

proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views); clarified Text.Range apartness, with try_restrict and try_join operations; private Perspective constructor to ensure abstract datatype integrity;

merged

tuned

merged

replacing metis proofs with facts xt1 by new proof with more readable names

more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies

disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction

NEWS

updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

removing redundant attribute code_inline in the code generator

tuned;

tuned;

improving mutabelle script again after missing some changes in f4896c792316

correcting code_prolog

merged

add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML

merged

tuned

mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties

merged

removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

removed [trans] concept from basic material

merged

tuned

merged

modernizing predicate_compile_quickcheck

adding depth as an quickcheck configuration

renamed name -> vname

removed some remaining artefacts of ancient SML code generator

NEWS

cleaner LEO-II extensionality step detection

marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs

one more LEO-II failure

merged

merged

hide typedef-generated constants Product_Type.prod and Sum_Type.sum

more uniform SZS status handling

avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"

merged

renamed B to Bc

tuned comment;

proper source positions for @{lemma};

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

tuned legacy signature;

further cleanup of stats (cf. 97e81a8aa277);

updated keywords;

really document just one code generator;

NEWS

removing old code generator

removing declaration of code_unfold to address the old code generator

removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const

removing documentation about the old code generator

removing old code generator setup for executable sets

removing old code generator setup for efficient natural numbers; cleaned typo

removing old code generator setup for real numbers; tuned

removing old code generator setup for rational numbers; tuned

removing old code generator setup for strings

removing old code generator setup for lists

removing old code generator setup for integers

removing old code generator for inductive predicates

removing quickcheck tester SML-inductive based on the old code generator