Relevant rules added to algebra's context

renamed item to span, renamed contructors; added span_range;

adapted ThyEdit.span;

maintain token range;

tty loop: do not report status;

added type range;

renamed command span markup;

SideKickParsedData: minimal content;

(adjusted)

(adjusted)

added verification framework for the HeapMonad and quicksort as example for this framework

build jedit plugin only if jedit is available;

misc tuning;

more class instantiations

refined code generator setup for rational numbers; more simplification rules for rational numbers

moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

fixed Scala path;

tuned build order;

proper purge_tmp; remove .cvsignore files;

tuned message;

tuned line breaks (NB: generated text is inserted here);

proper usage message; more precise perl replacements; less verbosity;

make Isabelle source distribution (via Mercurial);

explicit Distribution.changelog;

structure Distribution: swapped default for is_official;

ThyInfo.remove_thy;

structure Distribution: swapped default for is_official; removed obsolete (?) sync/sleep;

use ../isabelle.sty and ../isabellesym.sty;

tuned whitespace;

removed old checklist;

obsolete;

tuned;

discontinued maketags;

assume GNU tar and find; Admin/build all; discontinued maketags;

tuned;

use ../isabellesym.sty, which is always available;

Admin/build browser;

less verbosity;

Administrative build -- finish Isabelle source distribution.

simplified proofs

beautified proofs

added lemmas

Added Standardization theory to nominal examples.

Added Standardization theory.

editor model: run interactively for now;

updated generated file;

identify: more informative id in Toplevel.debug mode; interactive state transformations: dispose descendants *before* running next command, bypass for control commands; editor model: actually run affected commands; misc tuning;

shortlogentry/filelogentry: show shortdate and full description;

Removed uses of context element includes.

added Isar.command, Isar.insert, Isar.remove (editor model);

export type id with no_id and create_command; basic support for editor model: insert_command, remove_command; refined command status; misc tuning;

tuned;

renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

load thy_edit.ML before isar.ML;

modernized specifications and proofs; tuned document;

Removed uses of context element includes.

tuned

tuned code theorem bookkeeping

tuned changelogentry;

refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);

support for command status;

added status channel; writeln_default: suppress empty messages;

added status channel;

tuned;

simplified commit_exit;

simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;

removed obsolete commit_exit;

added command 'linear_undo'; tuned;

removed command 'redo'; added command 'linear_undo';

adapted ThyInfo.end_theory;

dropped map; fixed swap

curried gcd

cover macbroy as well; tuned;

tuned filelogentry;

print_mode "test_markup": do not change prompt, otherwise Proof General will not work;

tuned message;

updated generated file;

inform_file_processed: Isar.init_point last!

removed HOL-Complex, which has been discontinued after Isabelle2008;

added HOL-Nominal image;

removed obsolete Pure/General/history.ML;

inform_file_processed: try harder not to fail, ensure

commit_exit: proper error;

export EXCURSION_FAIL;

dropped junk

moved bootstrap of simplifier

tuned

end_theory: no result;

removed obsolete Toplevel.RESTART;

proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML); removed obsolete Toplevel.RESTART;

eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;

adapted IsarCmd.init_theory;

renamed theory to init_theory, removed obsolete kill argument; removed unused init_toplevel, begin_theory, end_theory; print_theorems: Toplevel.previous_node_of;

added commit_exit;

single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp

renamed conversions to _conv, tuned

Simplified proofs

Simple theorems about zgcd moved to GCD.thy

Theorem names as in IntPrimes.thy, also several theorems moved from there

Fixed proofs.

ProofNode.current

command 'redo' no longer available;

replaced obsolete ProofHistory by ProofNode (backtracking only);

removed obsolete 'redo' command; cannot_undo: global history; tuned;

removed obsolete history commands; moved back, cannot_undo to isar_syn.ML;

Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).

obsolete (cf. proof_node.ML);

removed Isar/proof_history.ML; added Isar/proof_node.ML

added further simple interfaces

simpsets as pre/postprocessors; generic preprocessor now named function transformators

unified curried gcd, lcm, zgcd, zlcm

Sorts.weaken: abstract argument; tuned;

Sorts.weaken: abstract argument;

instance real_field < field_char_0; instance star :: (field_char_0) field_char_0

re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef

Fract now total; improved code generator setup

simple inheritance concept

tuned thyname lookup

fixed layout

explicit completions of arities

tuned order

antiquotation

improved code generator setup

explicit dependency

class instead of axclass

tuned import

separate class dvd for divisibility predicate

temporarily disable at-sml-dev-p

updated generated file;

restart: Isar.init_point;

proper_inform_file_processed: Isar.init_point starts fresh command sequence;

activated new versions of undo, kill_proof;

activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;

added print;

added ProofGeneral.isar_kill_proof;

added Isar.init_point, Isar.kill;

export init_point; added kill, kill_proof; misc tuning;

added Isar.linear_undo;

tuned;

tty interaction: do not move point after error;

change_lexicons: no verbosity;

added Isar.undo, which emulates old-style undo on global tty state;

provide old-style undo operation (still unused); clarified command category; misc tuning;

added prompt markup;

@{lemma}: allow terminal method;

@{lemma}: allow terminal method, close derivation unless (open) mode is given;

added is_diag;

slightly improved @{lemma} (both for latex and ML); misc tuning;

misc tuning; more explicit error messages;

Fixed (harmless) typo in closing *}.

by intro_locales -> ..

instance real_field < field_char_0

remove redundant lemmas about cmod

removed owner;

tuned description;

changes wrt. gitweb style;

style = isabelle (based on gitweb);

rearrange instantiations

added get_first; tuned;

updated generated file;

updated generated file;

fix more typos

fix another typo

fix typo

updated generated file;

global commands: explicit graph; tuned;

export str_of;

clarified code

exported weaken combinator

refined arity property concept

fix: using IntInf.int for SML

moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; non-pervasive touch_thy, remove_thy;

removed obsolete touch_child_thys; simplified touch_thy, remove_thy, kill_thy -- inlined;

moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; removed unused touch_child_thys, touch_thy, remove_thy, kill_thy;

more qualified ThyInfo names;

begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear! replaced warning by error for non-existant theory/ML info;

removed unused href_opt_name; begin_theory: unconditional file links, proper output of parentheses;

migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware

retired mac-sml-dev.

absolute imports of HOL/*.thy theories

prefer theorem names without numbers

HOL-NSA

added marginal setup for code generation

use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero

removed old NSPrimes, cf. NSA/Examples/;

cvsps: back to non-verbose mode;

removed old Complex/ex/NSPrimes.thy;

maxfiles = 50;

more sessions;

more precise dependencies for HOL-Word and HOL-NSA;

fixed extremely slow proof of Chain_inits_DiffI

add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)

move proofs of add_left_cancel and add_right_cancel into the correct locale

cvsps -v (verbose);

removed nonstandard analysis theories to HOL-NSA

moved theories to HOL/NSA

add HOL-NSA

use patched cvsps to workaround loss of "foo: bar;" log entries;

move nonstandard analysis theories to NSA directory

back to default style, which shows files in changelog view;

added description;

tuned;

logrotate setup;

redirect stderr as well;

output to log file;

specific to CVS; some updates for Java etc.;

Isabelle repository service.

ensure hg/.hg/hgrc;

hgrc for conversion and web service;

provide HGRCPATH, taken from cvs/Admin; replaced MERCURIAL by HG, which is also used by Mercurial internally;

code antiquotation roaring ahead

tuned

adjusted postprocessort setup

added lemma antiquotation

adjusted rep_datatype

Adapted to changes in perm_simp / swap_simps.

Replaced all but one occurrence of perm_simp_tac by perm_simproc_app, since perm_simp_tac now behaves in a different way (due to changes in swap_simps).

Rewrote code to use swap_simps rather than calc_atm (which tends to produce ridiculously large nested if-expressions).

moved HOL-Plain up;

rename Doc doc-src;

renamed Contents to Dirs to avoid case-conflict with doc/Contents;

section -> subsection

convert Isabelle CVS to Mercurial;

use begin and end for proofs in locales