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