some theorems named explicitly

exported suffix

fixed typo

adjusted to current implementation

instance fun :: (finite, countable) countable

tuned

added Option_ord.thy

dropped local tsigs

some steps towards a refined treatment of equality

generic improvable syntax for targets

added hithero missing overloading.ML

tuned

whitespace tuning

clarified proposition

tuned proofs

canonical order on option type

added entries

check ISABELLE_BROWSER_INFO before cd;

replaced execute by system_out;

replaced execute by system_out;

added dummy version of string_of_pid;

use "ML-Systems/universal.ML"; specific system_out;

replaced execute by system_out;

proper dependency on ML-Systems/mosml.ML;

specific system_out (MosML lacks structure Posix); dummy implementation of Posix.ProcEnv.getpid;

* system/system_out provides a robust way to invoke external shell commands, with propagation of interrupts (after Poly/ML 5.2);

system_out: threaded version does not work for 5.1;

common setup for system_out/system;

added ML-Systems/system_shell.ML;

removed obsolete THIS_IS_ISABELLE_BUILD;

obsolete (cf. ML-Systems/polyml_common.ML);

renamed polyml-old-basis.ML to polyml_old_basis.ML;

rearrangements to make latest Poly/ML the default, not old 4.x;

cleaned-up ML-Systems;

tuned comment;

removed obsolete THIS_IS_ISABELLE_BUILD feature; moved external provers further up; no HOL4_PROOFS by default;

removed obsolete THIS_IS_ISABELLE_BUILD feature: change environment after getsettings (works due to static scoping);

removed obsolete THIS_IS_ISABELLE_BUILD feature;

removed obsolete THIS_IS_ISABELLE_BUILD/MAKEBIN feature;

renamed test_markup to output_markup; added full_markup mode, with token translations;

IsabelleProcess.output_markup;

closeup: minor tuning of term traversal;

ISABELLE_LINE_EDITOR: prefer rlwrap, which passes interrupts properly;

explicit referencing of background facts;

explicit referencing of background facts;

explicit referencing of background facts;

indexing literal facts: exclude background context;

put_thms: do not index facts here (affects prems/this/calculation in particular);

explicit referencing of background facts;

HOL/Library/RBT.thy;

NEWS: RBTs, renamings in ZF

Use conversions instead of simplifier. tuned

added new example

tuned

continued localization

new theory of red-black trees, an efficient implementation of finite maps.

Generalized Zorn and added well-ordering theorem

tuned ML code, more antiquotations;

misc cleanup of embedded ML code; use more antiquotations; tuned;

added @{const} antiquotation;

use more antiquotations;

unused_thms: print via official context (ProofContext.pretty_fact), not just the theory certificate (Display.pretty_thm); tuned;

Added function for finding unused theorems.

Added unused_thms command.

import all 'special code' types

added code generator setup

Transitive_Closure: induct and cases rules now declare proper case_names;

Transitive_Closure: induct and cases rules now declare proper case_names; tuned;

rtranclp_induct, tranclp_induct: added case_names; tuned proofs;

tuned

removed legacy ML bindings;

tuned syntax declaration;

wf_trancl: structured proof; tuned proofs; removed legacy ML bindings;

rtranclE, tranclE: tuned statement, added case_names;

renamed ListSpace to ListVector;

added HOL-Library;

more precise handling of "group" for termination;

added theories for imperative HOL

added theory for countable types

added theory for reflected types

proper merge of base sorts

Renamed ListSpace to ListVector

Fixed dependency on Dense_Linear_Order

removed some debugging output from trace

Loads Dense_Linear_Order (needed dlo_simps)

Fixed dependencies for proofs -- ferrack needed

Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.

fixed dependencies

Removed theorems from default simpset

Fixed proofs

Loads Dense_Linear_Order.thy

loads Tools/Qelim/qelim.ML

HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated

Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy

other UNIV lemmas

some more primrec

class itself works around a problem with class interpretation in class finite

moved some set lemmas from Set.thy here

tuned heading

char and nibble are finite

moved some set lemmas to Set.thy

tuned proofs

tuned document; tuned proofs;

tuned document;

Added useful general lemmas from the work with the HeapMonad

some steps towards automated generators

operation collapse

Zero/Suc recursion combinator for type index

added accidental omissions

thm_deps: sort result;

tuned msg;

fixed ChangeLog.gz path;

fixed document;

welcome: actually check for ChangeLog.gz; tuned structure Distribution;

tuned structure Distribution;

implicit use of LocalTheory.group etc.;

maintain group in lthy data, implicit use in operations; tuned signature; added group_position_of;

tuned;

LocalTheory.set_group for user command;

inductive package: simplified group handling;

Added dependency of Library on Pocklington.thy

Pocklington's Primality criterion

More primality theorems

A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales

A proof a the fundamental theorem of algebra

Uses Univ_Poly.thy

Does not import Poly anymore

Includes the derivates of polynomials -- reals specific content of Poly

Two simple theorems about cmod moved to Complex.thy

Now imports Funamental_Theorem_Algebra

Added trivial theorems aboud cmod

Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed

removed dead code; some cleanup

non-operative code antiquotation

non-operative code antiquotation

added further interface for reading constants

added first version of datatype antiquotation

moved refute_tac to linarith.ML

more elaborate structure Distribution (filled-in by makedist);

keep ChangeLog.gz within distribution; more elaborate structure Distribution (filled-in by makedist);

removed junk;

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some

removed NBE;

removed ex/NBE.thy;

fix proofs involving ile_def

tuned structures in arith_data.ML

using only an relation predicate to construct div and mod

now in AFP

added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);

removed General/system_process.ML (back to multithreaded version);

replaced setpgrp by more elaborate setsid;

slightly tuned

Yet another proof of False, this time using the strong case analysis rule.

tuned

system.pl - invoke shell command line (with robust signal handling);

updated

added eqvt-flag to subseteq-lemma

proved linorder and wellorder class instances

added get_parent (for AWE); tuned;

added perl wrapper for robust signal handling;

New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

removed spurious PolyML.makestring;

replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

removed managed_process (cf. General/shell_process.ML); replaced ignore/raise_interrupt by more flexible (un)interruptible combinators; tuned timeLimit: sleep already interruptible by default; schedule: restore attributes of body, instead of forcing interruptible execution;

removed managed_process (cf. General/shell_process.ML);

exn_message: added TimeLimit.TimeOut; replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

export deny_secure;

setmp: uninterruptible;

System shell processes, with static input/output and propagation of interrupts.

added General/system_process.ML;

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

support for managed external processes;

more lemmas

<= and < on nat no longer depend on wellfounded relations

moved *_reorient lemmas here

tuned names;

syntax error: suppress expected categories altogether;

expected syntax categories: reduced duplication, report minimal priorities only;

Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.

make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex

fixed record pretty printing

using integers for pattern matching

tuned whitespace

more abstract lemmas

fix spelling

imports Main;

removed unnecessary theory qualifiers;

simultaneous use_thys;

added Id;

Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).

tuned proofs and comments

tuned spaces;

tuned default position;

added default_properties;

added position_properties;

maintain default position;

overloading: reduced code redundancy, no xstrings here;

overloading: tuned signature;

Instead of raising an exception, pred_set_conv now ignores conversion rules that would cause a clash. This allows multiple interpretations of locales containing inductive sets.

fix broken syntax translations

use ML antiquotations

lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"

between constant removed

continued

locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder

replaced class by locale

*** MESSAGE REFERS TO 1.29 and 1.44 *** sort_of_term: be permissive about _class *output* markers, to allow print translations invoke this function as well;

towards quickcheck

suppport for messages and indices

added indexT

instance "*" :: (sq_ord, sq_ord) sq_ord

cleaned up

modified MCollect syntax

<TERM> syntax

fixed term_of_sort

fixed record problem

add lemmas prod_lessI and Pair_less_iff [simp]

add lemma is_lub_lambda

add lemma cpo_lubI

add lemma cpo_lubI

instances for class discrete_cpo

new lemma cont_discrete_cpo

new discrete_cpo axclass

temporary adjustions

explicit del_funcs

proper term_of functions

avoiding dynamic simpset lookup

new lemma is_lub_Pair; cleaned up some proofs

commented stuff out

added multiset comprehension

idempotent semigroups

dual orders and dual lattices

Theorem Inductive.lfp_ordinal_induct generalized to complete lattices

new term-building combinators

cleaned up evaluation interfaces

tuned names

treating division by zero properly

eliminated escaped white space;

basic scanners: produce symbol list instead of imploded string; tuned signature;

* Outer syntax: string tokens no longer admit escaped white space;

location_of_position: Position.column_of (which counts Isabelle symbols, not characters);

added count/counted: improved position handling for token syntax; removed obsolete incr_line/keep_line/scan_blank; string tokens no longer admit escaped white space, which was an accidental (undocumented) feature;

added column field; replaced inc by general advance operation; str_of: no output for file without line information;

T.count/counted: improved position handling for token syntax;

added column property;

removed redundant repeatd scanner combinator;

added ::: / @@@ scanner combinators;

Tuned uniqueness proof for recursion combinator.

Cleaned up simproc code.

tuned the proof of the substitution lemma

rename_client_map_tac: avoid ill-defined thm reference;

use_thy: do not set implicit ML context anymore;

added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;

renamed thms_containing_limit to FindTheorems.limit;

eliminated some legacy ML files;

added bind_thms;

tuned;

removed legacy ML file;

syntax error: unified output of priorities;

syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;

avoid redundant escaping of Isabelle symbols;

grouped versions of axioms/define/notes;

misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;

added theorem group property;

added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;

added surround;

tuned attribute syntax -- no need for eta-expansion;

added theorem group;

internal inductive: fresh theorem group;

modernized primrec;

Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections; more simultaneous use_thys;

modernized primrec;

tuned document; modernized primrec;

tuned document;

tuned;

* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;

tuned

print postprocessor equations

fixed and tuned

dropped superfluous code theorems

improved code theorem setup

consistent interacitve bootstrap of HOL-Main

distinguished examples for Efficient_Nat.thy

clarified setup of method "normalization"

moved definition of power on ints to theory Int

removed unused properties; replaced ContextPosition by Position.thread_data;

replaced ContextPosition by Position.thread_data;

statement: keep explicit position; replaced ContextPosition by Position.thread_data;

improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;

removed unused Toplevel.properties;

added combinator for wrapped lazy evaluation;

added setmp_thread_data_seq;

removed obsolete context_position.ML (superseded by Position.thread_data);

switched to polyml-cvs;

Reimplemented proof of strong induction theorem.

Added lemma at_fin_set_fresh.

reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;

exceptions: assign result = null properly;

tuned proofs;

recovered #der example without using val it;

yet another OCaml fix

tuned

added map_split

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;

removed unused of_stream; tty: Output.prompt, avoid low-level TextIO;

added explicit prompt channel (prompt_fn/prompt); tuned;

removed obsolete prompt and channel markups;

Tuned relevant premises selection

tuned comments;

added symbol output mode, with XML escapes; improved message markup: get first position from body text; added INIT message, with pid and session property; removed adhoc PID handling; tuned;

export session id;

secure_main: removed separate welcome;

removed unused text_charref, cdata; added plain_content;

added INIT message, with pid and session property; removed adhoc PID handling;

more instantiation

adhering to instantiation policy

cleaned up some proofs

simplified some proofs

partially adapted to new inversion rules

adapted to new inversion rules

fixed typo

improved warning

add new is_ub lemmas; clean up directed_finite proofs

new instance proofs for classes finite_po, chfin, flat

new lemma flat_less_iff

generalized chfindom_monofun2cont

Implemented proof of strong case analysis rule.

Added function fresh_const.

Added function partition_rules'.

another attempt to disable documents;

simplified position_props, always include line/file fields;

replaced thread_properties by simplified version in position.ML;

nested_command: simplified properties vs. position -- the latter also includes id now;

type T: based on properties, added id field; added thread_data, setmp_thread_data (formerly in toplevel.ML); tuned signature;

moved id to position properties;

instance unit :: finite_po

new axclass finite_po < finite, po

add lub_maximal lemmas; modify conclusion of directed_finiteD; declare not_directed_empty [simp]

added class Property: basic Isabelle properties;

tuned relevance test for presburger

output message properties: id or position;

toplevel print_exn: proper setmp_thread_properties;

added id property;

Result: added props field; tuned;

remove legacy ML bindings

new-style theorem references

fix theorem references

generalized and simplified proof of adm_Finite

new lemma adm_upward

Tuned (type information in Lemmas)

Changed order of tactics in presburger --- thinning before case splits

maintain thread transition properties;

setmp_thread_data;

added setmp_thread_data;

type transition: added properties field;

added properties;

Isabelle.command: IsarCmd.nested_command (with properties);

added nested_command (with explicit position argument via properties);

of_properties: return filtered result;

added method encodeProperties; method command/ML: pass Properties; tuned error messages;

setting -H 2000 and no documents for higher performance;

add dcpo instance proof

declare upE as cases rule; add new rule up_induct

update sq_ord/po instance proofs

move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type

remove not_up_less_UU [simp]

update instance proofs for sq_ord, po; new instance proofs for dcpo

add lemma ub2ub_monofun'

added dcpo instance proofs

new class dcpo; added dcpo versions of some lemmas

added new lemmas

add lemma dir2dir_monofun

tuned;

new is_ub lemmas; new lub syntax for set image

Multithreading.max_threads := 0 refers to number of cores of underlying machine;

added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

added usedir -M max (alias for -M 0);

new section for directed sets

split of class uminus

empty dictionaries for OCaml

clarified policy

tuned

some more antiquotations