proper signature constraint; modernized method setup;

minimal signature cleanup; modernized method setup;

modernized method setup; tuned;

modernized method setup;

tuned;

tuned;

simps with mandatory name prefix

corrected bound/unbounded flag for nat numerals

removed dead theory Relation_Power

fix reference to dist_def

definition of dist for complex

fix references to dist_def

define dist for products

move dist operation to new metric_space class

remove hard tabs, fix indentation

use class field_char_0

merged

generalize dist function to class real_normed_vector

added remark to code

Removed Convex_Euclidean_Space.thy from Library.

Moved some lemmas about intervals to Topology

Corrected definition of is_interval

corrected problem in Determinants

Corrected error in Convex_Euclidean_Space

Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile

merged

Added Convex_Euclidean_Space.thy

Changed prioriy of vector_scalar_mult

addition formulas for fps_sin, fps_cos

use class field_char_0 for fps definitions

merged

add constants sin_coeff, cos_coeff

merged

tuned signature of add_primrec_simple

added lemma select_weight_cons_zero

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