added class semiring_div

fixed OCaml

avoid 'it' in ML expressions

Removed Logic.auto_rename.

Efficient_Nat streamlined and improved

tuned proof

non-negative numerals

tuned

more lemmas

proper meaningful examples

explicit auxiliary function for code setup

streamlined and improved

adjusted to constant and theorem renames

avoiding direct references to numeral presentation

tuned code setup

add space to binder syntax

pcpodef generates strict_iff lemmas

change lemma admD to rule_format

improved implementation

convert lemma lub_mono to rule_format

rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less

change class axiom chfin to rule_format

change class axiom ax_flat to rule_format

joined theories IntDef, Numeral, IntArith to theory Int

tuned

further localization

explicit code lemma for implication

add instance for class bifinite

clean up some proofs; add lemmas spair_strict_iff, spair_less_iff, spair_eq_iff; add instance for class bifinite

declare cpair_strict [simp]

make at-sml-dev experimental

added bifinite class instance

add bifinite instances

add class bifinite_cpo for possibly-unpointed bifinite domains

cleaned up instance proofs

new-style instantiation proof for unit :: po

class bifinite supersedes class dcpo; remove unnecessary dcpo stuff

simplified chfin instance proof

new theory of powerdomains

new theory of bifinite domains

new-style class instantiation

added lemmas lub_distribs

*** empty log message ***

*** empty log message ***

compact_chfin is now declared simp

use new-style class for po

add lemma contI2

converted adm_all and adm_ball to rule_format; cleaned up

Equations for constants without arguments are now declared using "val" instead of "fun".

new theory defining set as a pcpo

Test data generation and conversion to terms are now more closely intertwined, to allow displaying of functions in test data.

New example involving functions.

Now uses more carefully designed simpsets to prevent proofs from failing for some strange datatypes with nested recursion.

Test data generation and conversion to terms is now more closely intertwined, to allow displaying of functions in test data.

Eliminated DatatypeAux.dest_TFree to avoid clashes with Term.dest_TFree.

Added nil_const and cons_const.

Added test data generator for function type (from Pure/codegen.ML).

New interface for test data generators.

declare ch2ch_LAM [simp]

added overloading target

new compactness lemmas; removed duplicated flat_less_iff

Compactness subsection with new lemmas

Compactness subsection with some new lemmas

new compactness lemmas

new lemmas max_in_chainI, max_in_chainD

overloading target

tuned

added simp attributes/ proofs fixed

added simp attributes

Finally: no more unproven.

tuned

some more primrec

tuned

a note on syntax in class context

a note on syntax

tuned proofs

normalization conversion

tuned comment

explicit type variables for instantiation

better error reporting

tuned

refined overloading target

imp_conv_disj is now declared as a "code unfold" lemma to avoid that conclusion is evaluated eagerly.

isabelle.jars: temporarily disabled, until isatest gets up-to-date java;

some pre-release tunings

more robust console thread (cf. jedit plugin version);

build Isabelle process wrapper; build jEdit plugin, if Scala is available;

* Rudimentary Isabelle plugin for jEdit;

added plugin installation;

tuned;

purge build directory;

basic setup for Isabelle/jEdit plugin;

added interface for command-line option;

removed obsolete prompt and channel markups; replaced prompt markup by prompt channel setup (avoids left-over XML encoding); tuned;

replaced prompt markup by prompt channel setup;

removed obsolete prompt markup;