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