dropped parentheses

parse translations for cases are conservative wrt. overloaded constructors

added generator for type copies (records)

adjusted to changed theory name

String.literal replaces message_string, code_numeral replaces (code_)index

moved Code_Index, Random and Quickcheck before Main

moved Code_Index, Random and Quickcheck before Main

pretty printing of functional combinators for evaluation code

new lemma

merged

FPS composition distributes over inverses, division and arbitrary nth roots. General geometric series theorem

merged

fine-tuned elimination of comprehensions involving x=t.

hide fact log_def -- should not shadow regular log definition

added example on ML level

added quickcheck support for numeric types

generalized lemma map_of_zip_map

added Code_Index.int_of operation

tuned term input syntax

merged

merged

merged

merged

experimental move of Quickcheck and related theories to HOL image

experimental addition of quickcheck

adjusted to changes in theory Quickcheck

combinators for single-threaded operations

tuned code postprocessor

dropped theory Term_Of_Syntax

hide names in theory Random

experimental addition of quickcheck

syntax support for term expressions

introduced Thm.generatedK

is a definition

merged

added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages

merged

added collection of simplification rules of recursive functions for quickcheck

merged

added predicate transformation function for code generation

added predicate transformation function for code generation

proof tuned

merged

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".

merged

continuity proofs for approx function on deflations; lemma cast_below_imp_below

allow lazy domain arguments to have class cpo

add cpo_type function

fix domain package parsing of lhs sort constraints

export quiet_mode and trace_domain refs for domain package

new lemma

merged

merged

merged module code_unit.ML into code.ML

monomorphic code generation for power operations

preprocessing must consider eq

quickcheck size starts with 0

strip sorts while checking pattern subsumption

rewrite op = == eq handled by simproc

updated generated document

merged

Cleaned up Parity a little

merged

merged

Cleaned up code of function test_term.

dropped accidental debug messages

adapted code tutorial to recent changes in code

more permissive wrt. overloaded constants

merged

tuned construction of term_of instances

tuned construction of term_of instances

dropped legacy operations

tuned construction of typerep instances

tuned and generalized construction of code equations for eq; tuned interface

added abstract operations for typerep/term_of

tuned and generalized construction of code equations for eq

dropped sort constraint on predicate equality

itself is instance of eq

Now deals with division

updated keywords

split Predicate_Compile examples into separate theory

adapted to changes in module Code

values is now a keyword

merged

transferred code generator preprocessor into separate module

marginally tuned

examples using code_pred

added dummy values keyword

tuned exception code

A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination

A decision method for universal multivariate real arithmetic with add ition, multiplication and ordering using semidefinite programming

Isolated decision procedure for noms and the general arithmetic solver

Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library

merged

use Pair/fst/snd instead of cpair/cfst/csnd

use Pair/fst/snd instead of cpair/cfst/csnd

move bifinite instance for product type from Cprod.thy to Bifinite.thy

new lemmas

fixed merge accident

merged

avoid latex output problem

merged

fixed code_pred command

Added pred_code command

added general preprocessing of equality in predicates for code generation

merged

merged

mk_number replaces number_of

qualified names for Lin_Arith tactics and simprocs

tuned interface of Lin_Arith

optimized Approximation by precompiling approx_inequality

replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith

merged

newline at end of file

simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules

removed redundant instance declarations inat :: linorder

merged

proper error handling for malformed code equations

corrected deletetion of code equations for constructors

clarified matter of "proper" flag in code equations