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

tuned interface of module Code_Unit

clarified terminilogy concerning nbe equations

simplified unoverload/overload policy in code generator preprocessor

Change to lowercase path names as directed by local pagemasters

merged

fixed HOLCF proofs

merged

interface changes in linarith.ML

merged

lemmas by Andreas Lochbihler

merged

merged

more lemmas

rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names

fixed theorem statement

merged

Generalized distributivity theorems of radicals over multiplication, division and inverses

proper structure name

localized (complete) partial order classes

dropped legacy ml theorem binding

modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs

modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs

generalized simproc for mod

explicit method linarith

moved int_factor_simprocs.ML to theory Int

treat frees driectly by the LCF kernel

dropped explicit suppport for frees in evaluation conversion stack

no need for explicit delete declaration

better to have distinguished class for preorders

added theory for explicit equivalence relation in preorders

explicit type_name antiquotations

explicit type arguments in constants

merged

robustifed infrastructure for complex term syntax during code generation

proper structures for list and string code generation stuff

explicit type arguments in constants

confine term setup to Eval serialiser

adaptation replaces adaption

refined HOL string theories and corresponding ML fragments

adaptation replaces adaption

explicit type arguments in constants

refined HOL string theories and corresponding ML fragments

tuned description of overloading

confine term setup to Eval serialiser

updated generated file

new lemmas

merged

Prototype introiff option for find_theorems. This feature was suggested by Jeremy Avigad / Tobias Nipkow. It adds an introiff keyword for find_theorems that returns, in addition to the usual results for intro, any theorems of the form ([| ... |] ==> (P = Q)) where either P or Q matches the conclusions of the current goal. Such theorems can be made introduction rules with [THEN iffDx]. The current patch is for evaluation only. It assumes an (op = : 'a -> 'a -> bool) operator, which is specific to HOL. It is not clear how this should be generalised.

replace cont2cont_apply with cont_apply; add new cont2cont lemmas

compatible with preorder; bot and top instances

updated generated files etc/isar-keywords.el and lib/jedit/isabelle.xml

tuned

added Philipp Meyer's implementation of AtpMinimal together with related changes in the sledgehammer-interface: adapted type of prover, optional relevance filtering, public get_prover for registered atps in AtpManager, included atp_minimize in s/h response;

removed code_name module

desymbolization with case selection

dropped duplicate lemma sum_nonneg_eq_zero_iff

fixed broken link

tuned header

class typerep inherits from type

use simproc_setup command for cont_proc

used named theorems for declaring numeral simps

clean up unsigned numeral proofs

detect error cases in mk_num, dest_num

add semiring_assoc_fold simproc for unsigned numerals

reorient simproc for unsigned numerals

reimplement reorientation simproc using theory data

use opaque ascription for all HOLCF code

added listsum lemmas

farewell to class recpower

merged

power constraint needed, though

stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy

stripped class recpower further

lemma sum_nonneg_eq_zero_iff

reorganization of power lemmas

collected square lemmas in Nat_Numeral

Symbol.name_of and Name.desymbolize

prevent potential failure

ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms

local syntax for Ints; ephermal re-globalization

dropped reference to class recpower and lemma duplicate

add proper support for bottom-patterns in fixrec package

merged

add module signature to domain_library.ML

add module signature for domain_theorems.ML

declare take_rews as simp rules

explicit is better than implicit

whitespace tuning

cleaned up theory power further

merged

merged

merged

fixed document generation

cleaned up Power theory

merged

merged

merged

more general statements

tuned

reorganised the section about fresh_star and added lemma pt_fresh_star_pi

reverted slip in theory imports

adjusted to changes in power syntax

merged

deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means

append prefs at end;

merged

adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)

use predefined preferences categories;

removed obsolete artifacts;

misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;

renamed contrib/SystemOnTPTP/remote to lib/script/SystemOnTPTP, thus leaving contrib empty within the official distribution;

post Isabelle2009 version;

adjusted to change in code_wellsorted.ML

merged

some jokes are just too bad to appear in a theory file

removed confusion around funpow

observe distinction between Pure/Tools and Tools more closely

some experiements towards user interface for predicate compiler

funpow and relpow with shared "^^" syntax

generic postprocessing scheme for term evaluations

added helpless comment

adaptions due to rearrangment of power operation

stripped $Id$

avoid local [code]

dropped duplication

code_datatype and power

tuned

code_datatype antiquotation; tuned

more localisation

power operation defined generic

fixed compilation of predicate types in ML environment

merged

merged

empty page leads to results on duplex printers as expected

changes in power operations

power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure

yield is now a static ML function

power operation on functions with syntax o^; power operation on relations with syntax ^^

formal declaration of undefined parameters after class instantiation

power operation on relations now with syntax ^^

separated funpow, relpow from power on monoids

static compilation of enumeration type

re-engineering of evaluation conversions

tuned

separate channel for Quickcheck evaluations

merged

zmod_zmult_zmult1 now subsumed by mod_mult_mult1

diagnostic commands now in code_thingol; tuned code of funny continuations

simplified code

zmod_zmult_zmult1 now subsumed by mod_mult_mult1

added both cancel_div_mod_procs

wellsortedness is no issue for a user manual any more

whitespace tuning

added simproc

dropped unnamed infix

tuned setups of CancelDivMod

merged

tuned order of functions

generalized some simprocs from int to semiring_div

tightended specification of class semiring_div

code generator bootstrap theory src/Tools/Code_Generator.thy

say farewell to code related to old code_funcgr module

wrecked old code_funcgr module

index type is a semiring_div

theory NatBin now named Nat_Numeral

default instantiation for unit type

more coherent developement in Divides.thy and IntDiv.thy

add more examples to Domain_ex.thy

merged

add HOLCF/ex/Domain_ex.thy, with example uses of the domain package

make domain package ML interface more consistent with datatype package; use binding instead of bstring

use Sign.add_consts instead of ContConsts.add_consts

merged

allow infix declarations for type constructors defined with domain package

remove obsolete comments

fix too-specific types in lemmas match_{sinl,sinr}_simps

domain package now generates iff rules for definedness of constructors

change definition of match combinators for fixrec package

domain package: simplify internal proofs of con_rews

set up domain package in Domain.thy

tuned proof

replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.

inlined afterqeds to improve clarity; tuned

simplify computation and consistency checks of argument counts in the input

removed obsolete test tags;