setup_goal: proper handling of non-atomic goals (include cprems into asms);

Isabelle manuals now also available as PDF;

move pdfs back into dist;

pdf docs;

separate archive for pdf docs;

\def\bold;

tuned formal comments;

tuned manual.bib;

changed {| |} verbatim syntax to {* *};

changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;

improved undo / kill operations;

fixed corruptoin of end of file

removal of Always_StableI

replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre, Always_Constrains_post

component_eq_subset: a neat characterization of "component"

ex/Points Isar'ized;

local_qed: print_result;

cannot_undo; qed_block keywords;

cannot_undo;

qed_block keywords;

local qeds: pass cond_print_result;

cleaned comments; local_qed: print_result argument; prep_result: always varify type variables (Thm.varifyT);

new theories Follows and ListOrder

formal comments (still dummy);

added formal comment arguments almost everywhere (still ignored);

renamed Comment.empty to Comment.none; added P.marg_commend almost everywhere;

renamed Comment.empty to Comment.none;

renamed empty to none; added ignore, ignore_interest, ignore_interest';

fixed cvs Id;

outer syntax keyword classification; no open OuterParse;

added keyword classification;

tuned print_context;

write_keywords generates outer syntax keyword classification in elisp;

outer syntax keyword classification; no open OuterParse;

renamed Lprg to Lift; simplified proof of Always_nonneg

int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc

Better simplification of (nat #0), (int (Suc 0)), etc

UN_singleton->UN_constant_eq removes clash with other UN_singleton

new rule single_leadsTo_I; stronger PSP rule

increasing makes sense only for partial orderings

generalized increasing_size to mono_increasing_o

updated for stronger version of psp

new rule single_LeadsTo_I; stronger PSP rule; PSP_stable2->PSP_Stable2

expandshort

lists are partially ordered by the prefix relation

using generic rules when possible

Theory of the "Follows" relation

Increasing makes sense only for partial orderings

generalized Increasing_size to mono_Increasing_o

tidied

renamed PSP_stable2->PSP_Stable2

now uses mono_Increasing_o

updated for stronger version of psp

Configuration for ProofGeneral of LFCS Edinburgh.

Configuration for David Aspinall's Isamode.

Miscellaneous interfaces.

Isamode.setup, ProofGeneral.setup;

Isamode and ProofGeneral configuration moved to Pure/Interface;

added use_thy_only;

added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;

avoid string constants;

qed indexed.

typedef_proof: pass interactive flag;

tuned; added prompt_state_fn hook; added kill operation; provide toplevel node history, nests with proof history; toplevel prompt includes nest level; more robust recovery from stale signatures;

cleaned comments; global statements: init history according to interactive mode; local qed: pass interactive mode; init theory: kill operation;

renamed 'begin' / 'end' to '{{' / '}}'; added 'kill'; rename 'type' to 'typ';

history commands;

tuned;

adapted to History changes;

local_qed: obtain interactive flag;

backup replaced by checkpoint;

added default_prompt; removed decorate_prompt_fn hook;

optional limit; is_initial; apply_copy, map;

improved errors;

updated comment

made definition more readable

preferring generic rules to specific ones...

changes to show that Lists are partially ordered by the prefix relation

deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)

redid proofs to use "always" rather than "reachable" (somewhat)

new theorem Always_reachable

tuned;

added Locale paper

locale documentation (from Florian)

../manual.bib a new dependency

cleaned comments;

cleaned comments; ThyInfo.finalize_all renamed to ThyInfo.finish; added remove_thy;

tuned;

cleaned comments; node_cases renamed to node_case; more robust rollback of transactions via backup;

ThyInfo.finalize_all renamed to ThyInfo.finish;

node_cases renamed to node_case;

prep_ext exported (again);

backup operation replaces transaction;

removed get_nodes; added keys; all_preds / all_succs: topological order; added del_nodes;

remove_thy;

tuned arrows;

Arrows are no longer needed because of redesign of the html pages.

Changed some file names.

Added function get_preds.

Added setup for BrowserInfo.

usedir now recognizes additional option -P which is used to tell the presentation module where to find *.html files of theories.

Changed interface of function use_dir.

Present.begin_theory now needs an additional argument of type theory to store information about session identifiers.

Reimplemented graph generator.

Added some code to enable browser to display remote documents.

new thm extend_JN; renamed extend_leadsto

"component" now an infix

indentation

tuned;

ad-hoc fix for bold indexes;

strip_quotes replaced by unenclose;

rearranged some modules;

rearranged order of modules;

Basic URLs.

added url.ML;

pdf setup;

tuned;

fixed msg;

moved scan.ML;

new comments, variable renaming, etc