added lemma beyond_zero; hide constants

added lemma about 0 - 1

merged

more lemmas

merged

add_primrec_simple

dropped superfluos prefixes

separate module for quickcheck generators

encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas

listsum lemmas

clean up some rsum proofs

weakend references to old axclass

clarified benefit of interpretation

documented print_codeproc command

use interval sets with gauge predicate

clean up some proofs

tuned whitespace

funpow_yield; tuned

tuned class user space type system code

dropped Id

refined construction_interpretation

exported find_shorzes_path

merged

fixed superficial ML lapses introduced in b3c7044d47b6;

simplified method syntax;

modernized method setup;

modernized method setup; tuned signature;

proper signature constraints; modernized method setup;

adapted to Poly/ML SVN 744;

removed some obsolete combinators for method args;

proper indentation;

proper signature constraint; observe basic Isabelle/ML coding conventions, concerning parentheses, whitespace, indentation, and max. line length;

adapted to Poly/ML SVN 719; removed obsolete add_prefix;

getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);

merged

define copy functions using combinators; add checking for failed proofs of induction rules

export ID, oo; add more dtyp operations

add combinators for building copy functions

change representation of Domain_Library.arg

make type Domain_Library.arg abstract

indentation; export Domain_Axioms.calc_axioms

indentation; export Domain_Syntax.calc_syntax

using precompiled Predicate.map

merged

re-added corrected version of type copy quickcheck generator

added Predicate.map in SML environment

merged

implementation of definitional CNF improved

write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first

fixed typo

experimental values command

added Predicate.map

merged

tuned

adjusted to changes in Quickcheck.thy

eliminated case input syntax on bits

removed quickcheck generator for type copies temporarily

avoid potential problem with stale theory

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