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;

back to non-release mode;

Added tag Isabelle2009 for changeset 5c8618f95d24

merged

give up file type / dropability for now -- does not work reliably; tuned;

Added tag isa2009-test for changeset d394a17d4fdb

external_prover: "exec" the command line, in order to preserve the exact process context of the "system" invocation (this recovers interruptibility of E-1.0, which assumes to be the process group leader);

misc tuning for Isabelle2009;

tuned;

more generic error message, which also covers more fundamental failure;

updated for Isabelle2009;

tuned;

more robust handling of emacs options -- this is not necessarily an Isabelle process environment yet;

merged

actually invoke ISABELLE_TOOL;

added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;

ISABELLE_USEDIR_OPTIONS: less ambitious -M1 by default -- multithreading is largely untested on fringe platforms (cygwin, solaris);

misc updates for Isabelle2009;

Added tag isa2009-test for changeset dda08b76fa99

updated official title of contribution by Johannes Hoelzl;

misc tuning and updates;

updated doc setup;

merged

moved generated eps/pdf to main directory, for proper display in dvi;

updates for E-1.0-004;

tuned manual

merged

tuned comment

Added tag isa2009-test for changeset 613c2eb8aef6

tuned whitespace

merged

reverted to explicitly check the presence of a refutation (compare to 479a2fce65e6); simplified handling of errors in remote script

tuned white space;

merged

\nolinkurl for dvi mode recovers hyphenation of URLs -- this already works by default in PDF mode;

removed obsolete website directory -- information derived by website/build;

More precise treatement of rational constants by the normalizer for fields

fixed usage of rational constants

No Complex_Main needed

now deals with devision in fields

fixed formal markup;

merged

Finite_Set: lemma IsarRef: attribute arith

single-threaded build; misc tuning and simplification;

merged

Added check whether argument types of inductive set agree with types of declared parameters to avoid low-level error messages.

added setsum_eq_1_iff

simplified website/config;

Updated to corrected E output messages

updated keywords (with polyml-experimental);

some more HOL-Nominal news;

merged

tuned signature;

misc tuning for release;

merged

Fixed bug in transformation of congruence rule for == (thanks to Andy Schropp for reporting this).

some HOL-Nominal news;

updates for Isabelle2009 release;

tuned;

merged

misc cleanup and rearrangements for Isabelle2009 release;

merged

cleaned up setprod_zero-related lemmas

merged

generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs

added nat_div_gt_0 [simp]

added setsum_pos_nat

merged

added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas

proper external tikz pictures

merged

tuned comments;

merged

explicitly check that at least one argument is present to avoid low-level exception

merged

included managing_thread in state of AtpManager: synchronized termination and check for running managing_thread

domain package registers induction rules

merged

Merged.

Improvements to the text.

fixed header; misc simplification, use Conjunction.dest_conjunctions;

fixed header;

added dest_conjunctions (cf. Logic.dest_conjunctions);

superficial tuning;

merged

merged

schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;

updated latex requirement;

tuned document;

replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp); modernized and tuned document;

tuned error message;

tuned;

suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;

generalized pull to anamorph

merged

ML snippets for experimental evaluation

merged

merged

domain package declares more simp rules

simplified 'print_orders' command;

tuned;

merged

merged

simplify theorem references

added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);

tuned spacing and formatting;

merged

terminate watching thread

merged

no longer delay loading of assoc_fold.ML

qualified_name_of: observe empty case;

merged

merged

add more lemmas for signed comparisons

use standard parsers provided by SpecParse

bstring -> binding

code attribute for tailrec-equations, too; tuned

optimistically add code attribute to .simps without further checks

remove "otherwise" feature from function package which was never really documented or used

prep_full_context_statement: explicit record of flags; prep_declaration (for add_locale): disallow autofixed frees;

Limit the number of results returned by auto_solves.

merged

Merged.

In interpretation: equations are not propagated through the hierarchy automatically.

Normalise equation only for morphism, not thm stored in theory.

Default mode of qualifiers in locale commands.

Front matter updated.

tuned;

simplified Element.activate(_i): singleton version;

tuned;

added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;

unified binding prefix terminology;

simplified roundup activation interface;

merged

merged

merged

second attempt for code_deps command

merged

corrected projection of required statement names

corrected check for additional type variables on rhs of code equations

not yet fruitful tex experiments with bounding boxes

simplified Locale.activate operations, using generic context; misc tuning;

renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;

define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;

renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;

simplified references to facts, eliminated external note_thmss;

added map_facts_refs;

tuned;

replaced add_binds(_i) by bind_terms -- internal version only;

replaced add_binds by singleton bind_term;

simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;

minor tuning;

merged

Merged.

Corrections to locale syntax.

Update explanation of locale expressions to locale reimplementation.

Comments updated.

fixed proof

merged

fps made instance of number_ring

updated keywords with polyml-experimental;

export position_of;

dropped infix union

tuned notoriously slow metis proof

merged

dropped toy example Code_Antiq

more convenient name uniqueness

normalized imports

dropped legacy goal package call

merged

merged

step towards proper pictures in dvi

merged

parameterize assoc_fold with is_numeral predicate

merged

New theorems mostly concerning infinite series.