oops;

added order_le_less_trans, order_less_le_trans;

Calculation.thy: Setup transitivity rules for calculational proofs.

Support for calculational proofs.

added put_st;

added the_fact, level;

export multi_resolve;

added also, finally;

added 'also', 'finally' commands;

added COMP attribute;

added calculation.ML;

added Isar/calculation.ML;

fixed BUG in have_thmss: return thy';

added dest_main_statement;

print "..." variable;

no message "Adding axioms for datatype(s)";

added Group.thy;

added Isar_examples/Group.thy;

Some bits of group theory. Demonstrate calculational proofs.

read_term/prop_pat: do not freeze;

added dddot_tr;

added dddot_indexname;

"..." syntax;

find -print;

'kill' made improper;

improved print_state;

'note': Toplevel.print;

tuned markup;

broder size 3;

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;