cond_extern_table;

added presume command;

cond_extern_table; datatype method = Method of thm list -> tactic;

tuned print_state; datatype method = Method of thm list -> tactic; assumptions: back-pressure solver as parameter;

tuned output: print_context replaced by strings_of_context; assumptions: back-pressure solver as parameter;

cond_extern_table;

added cond_extern_table;

branching_level = 400;

tidied

renamed PPI to plam simplified the definition of lift_act

renamed PPI to plam

another non-working snapshot

new distributive laws involving * and -

rewrite rules to distribute CONSTANT multiplication over sum and difference; removed automatic rewriting of 2x to x+x

another snapshot, still not working

new results about SKIP

addition of drop_... operators with new results and simplification of old ones

renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)

many new guarantees laws

moved image_UNION to Fun/image_UN

expandshort

renamed UNION_... to UN_... (to fit the convention)

renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT

not working but taking shape

guar; locale for the spec

many new results for reachable and lift_prog

new finiteness theorems

renamed pfix_[lg}e

new-style infix directives

guarantees -> guar

guarantees -> juar

rev=rev lemma.

fixed title line; added spacing

no longer needs ../Lex

new UNITY files

unclosed comment.

The Allocator example: specifications

expandshort

many new lemmas about take & drop, incl the famous take-lemma Ran expandshort

moved predicates refl, sym down to Relation.thy

Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra

using the new GenPrefix theory

shortened Follows to Fols

tidied

new translation to allow images over Nonce

new preficates refl, sym [from Integ/Equiv], antisym

new lemma less_Suc_eq_0_disj

Generalized prefix theory, replacing the reference to directory Lex.

Stefan Merz's lemmas.

added square root example.

renamed the underlying relation of leadsTo from "leadsto" to "leads" to reduce the risk of confusion

removed obsolete "Prefix" ancestor

new classical example from Lewis Carroll via S G Pulman

tuned mode_name; improved handling of assumptions; eliminated let_thms (named prop bindings moved to auto_bind.ML);

improved handling of assumptions;

facts: bind named props (from proof.ML/let_thms);

reset HOL_quantifiers by default;

Added lots of 'replicate' lemmas.

groups as monoids; tuned;

tuned comments;

added Ord.order_antisym;

auto_bind_goal, auto_bind_facts; varify_tfrees: no longer generalize types of free term variables; let_thms: no bindings;

auto_bind_goal, auto_bind_facts;

added get_st;

tuned;

varifyT': observe additional 'fixed' tfrees;

removed ObjectLogic.setup;

proper calculation;

renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;

fixed "...": dest_arg;

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;

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

tidied

changes for new manual.bib

make pdf;

tuned;

pdf setup;

cite HOLCF;

tuned;

axclass;

axclass; datatype;

pdf setup;

*** empty log message ***

*** empty log message ***

pdf setup;

fixed URLs;

pdf setup;

replaced png by pdf;

pdf pics;

tidied

tidied

new refererences for Inductive manual, but still incomplete

tuned;