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;

pdf setup;

*** empty log message ***

pdf setup;

tuned;

More refs.

Refs.

New title page.

tuned;

manual.bib;

no rail;

fixed FILES;

improved Makefile;

improved Makefile;

isabelle.eps;

improved Makefile; no rail;

tuned;

improved Makefile;

*** empty log message ***

Common part for Doc Makefiles;

Now uses manual.bib; some references updated

tuned rpm file names;

updated docs;

Bibtex database for documentation.

Bibtex stuff.

*** empty log message ***

HOL;

removed HOL.tex;

tuned;

updated;

HOL part moved to 'logics-HOL' manual;

fixed;

used to be part of 'logics' manual;

isabelle_zf image;

*** empty log message ***

Arithmetic.

add_recdef: removed names / attributes;

new definitions of Co and LeadsTo

transaction: Theory.copy;

hide prep_ext, merge_theories;

oops;

tuned;

Invariant -> Always and other tidying

tuned;

theory loader stuff updated and improved;

fixed reqs?

improved error handling

renamed state variables

tidied

tuned;

prefer /bin for ./configure;

try chown root:root;

renamed 'dummy' to 'dummy_pattern' (less dangerous);

tuned;

method = meth3 (again);

peoper defer_recdef interface;

theory data: copy;

separated recdef / defer_recdef;

tuned defer_recdef interfaces;

comment, interest;

Comment.text;

comment sections; made "%" a keyword;

dummy patterns; theory data: copy;

added Isar/comment.ML;

val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;

theory data: copy; consts dummy :: 'a ("'_");

theory data: copy;

improved icons;

Isabelle icons;

patched sum_case;

Obsolete because JDK 1.1.x contains a class ScrollPane

Updated to JDK 1.1.x

Proof mods due to eta contraction during rewriting.

Eta contraction is now performed all the time during rewriting.

currently disabled;

*** empty log message ***

made many specification operators infix

eliminated theory UNITY/Traces

improper simp methods;

tuned;

fold / unfold methods;

tuned;

no Toplevel.print for by, ., ..;

improved print_state;

verbose flag;

use_thy_only made pervasive;

added Isar_examples/NatSum.thy;

Old stuff.

proper quiet_mode; tuned messages;

adapted add_inductive, add_record;

adapted add_inductive;

intrs attributes;

proper quiet_mode;

iff_add_global (from simpdata.ML);

support forward chaining;

tuned;

added Isar_examples/Cantor.ML;

hol_setup, simpdata_setup;

"iff" attribute; simpdata_setup;

hol_setup;

"!" made keyword;

opt_thm_name: name optional;

added oooo;

fixed a bug many years old in rule plusEC

tuned msgs; outer syntax;

tuned;

tuned;

elaborated;

tuned;

tuned antiquotations;

improved 'single' method; added 'contradiction' method;

added thus, hence;

added FINISHED, same_tac;

use /usr/share and /usr/bin;

Now for recdefs that omit the WF relation; removed the separation between draft and theory modes

Now for recdefs that omit the WF relation

Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml

chgrp isabelle;

detailed proofs;

tuned;

oops;

fixed IO;

improved load paths;

single method: include not_elim, imp_elim;

more graceful handling of load paths;

improved auto dir handling;

tuned;

make Isabelle rpm packages for Linux/x86 from the distribution;

use_thy etc.: may specify path prefix, which is temporarily used as load path;

switch_theory: Context.pass;

recdef (TFL) now requires theory Recdef;

recdef requires theory Recdef;

tuned;

rep_datatype syntax: 'induction' instead of 'induct';

add_recdef: actual simpset; add_recdef_x: named simpset;

recdef adapted to RecdefPackage.add_recdef;

Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;

added ex and Modelcheck

tuned;

added for mucke translation;

deleted some old examples in Modelcheck;

added translation from IOA to mucalculus and corresponding modelchecker examples;

moved this trivial example to new ex dir;

changed to include new subdirs ex and Modelcheck;

put types into "" because of signature clash;

added frontend syntax for IOA, moved trivial examples to folder ex;

added modelchecker mucke besides modelchecker eindhoven;

delete old files for adding second modelchecker connection;

$ML_HOME/.arch-n-opsys 2>/dev/null;

smlnj-110 setup made default;

/usr/share/smlnj/bin;

Isamode 2.6 requires patch;

added is_current;

fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;

temporarily fake quiet_mode;

temporarily reverted to 1.24;

IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly) provided HIGHER-ORDER logic

Main is the correct parent

new result extend_LeadsTo

should not refer to Datatype

addition of Kerberos IV example

tidied

improved usage;

loadpath replaced;

and_list;

lifted enum; removed list(1); added and_list(1);

may specify induction predicates as well;

added Isar_examples;

Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

lemmas about proper subset relation;

Proof by induction on types / set / functions.

print_datatypes;

added Tools/induct_method.ML;

'HOL/recdef' theory data;

'HOL/recdef' theory data; induct method setup;

'HOL/inductive' theory data;

Sign.base_name fid;

added incr_indexes, incr_indexes_wrt;

Proof mod.

Added new thms.

quiet_mode;

Tools/inductive_package.ML;

triple_swap;

Wrapper module for Konrad Slind's TFL package.

remoced old set_current_thy;

tuned messages;

intrs: names and atts;

tuned comments; tuned types;

tuned comments; intrs: names and atts; Isar outer syntax;

tuned comments;

intrs: provide names and atts;

cleaned comments;

tuned;

fixed named type infixes (actual BUG!);

updated isatool install;

-p option; -k option;

adapted isatool install;

improved isatool install;

tuned;

ML_PLATFORM;

ML_PLATFORM;

fixed @@;

fixed bib file

fixed;

new definition for nth. added warnings, if primrec definition is deleted from simpset.

useless relic

arith_tac

tuned;

common qed and end of proofs;

* New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

New bounded quantifier syntax: !x<i. P etc

added new theory Yahalom_Bad

added new theory Yahalom_Bad

exchanged the order of Gets and Notes in datatype event

fixed thm_name again;

Theory.sign_of;

xnum token class;

xstr token class;

Theory.sign_of;

fixed axclass_tac;

tuned;

Theory.sign_of;

qualify Theory.sign_of etc.;

fixed msg;

tuned msg;

axclass_tac lost an argument;

HOL/typedef: fixed type inference for representing set; AxClass.axclass_tac lost the theory argument;

rep_datatype: '_i' version, attributes, outer syntax;

local open OuterParse;

actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax;

fixed typedef representing set;

adapted rep_datatype;

added dest_mem;

theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;

adapted AxClass.add_axclass; PureThy.get_thm axioms;

tuned msgs; removed verbose flag;

tuned;

cleaned comments;

added apply_cond_open;

added (improper_)command;

added simple_arity, spec_name, spec_opt_name; tuned thm_name; xthms1: no 'and' separators;

added '_i' versions; add_constdefs; apply_theorems; fixed assume block nest;

OuterSyntax.(improper_)command; moved axclass / instance to Pure/axclass.ML; moved spec(') to outer_parse.ML;

added assert_super;

added def_name; class_triv: Sign.sg;

added cond_extern_thm_sg; have_thmss: name made optional;

AxClass.setup;

axclass.ML loaded after Isar;

made weblint happy;

comment;

removed obsolete user data stuff; removed junk;

theory: include parent links;

outer syntax for 'datatype';

add_primrec(_i): attributes; outer syntax for 'primrec';

outer syntax for 'record'; proof method 'record_split';

named witnesses: PureThy.get_thmss; outer syntax for 'typedecl', 'typedef';

primrec: empty attributes;

tuned opt_mixfix failure;

add_title;

added 'title'; tuned names, comments;

tuned space;

comment;

workaround default_name problem;

removed foo_build_completed -- now handled by session management (via usedir);

include 'README'; tuned;

tuned;

moved Thy/session.ML to Isar/session.ML;

tuned;

-x option;

updated;

report session path; removed more junk;

report path instead of actual session;

HTML output;

maintain current/parent index; removed junk;

output: some symbol translations; removed insert_here, conclude_theory; added begin/end_index, theory_entry, session_entries;

parent_session;

allow meta_outer to do nothing

updating both Yahalom protocols to the Gets model

updated not_bad_tac for the Gets model

deleted obsolete comments

Present.theory_source;

begin/end_theory: presentation;

checkpoint -- basic functionality only;

added use_path; begin_theory: include files;

IsarThy.begin/end_theory;

Present.theorem;

fixed add_path reset; init / finish presentation;

still fake, passes BrowserInfo;

HTML markup elements.

added html.ML, browser_info.ML;

token translation: real;

added strlen_real, setmp_margin;

tuned using nth_elem_string, exists_string;

added make, dir;

added mkdir;

added Buffer;

simple string buffers;

*** empty log message ***

pretty_thm_no_quote;

HTML.setup;

added nth_elem_string, exists_string;

token translation: real;

tuned;

tidied

Added Bella's "Gets" model for Otway_Rees. Also affects some other theories. Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a translation.

Suc -> +1

modified zip

Fixed bug in add_datatype_axm: Recursion and case combinators were assigned inconsistent names in quick_and_dirty mode, which caused recdef etc. to crash.

fixed again;

expandshort

added UNITY/Extend

expandshort

tidied

UNITY fully working at last...

expandshort

new theory of extending the state space

fixed {ISABELLE};

removed the infernal States, eqStates, compatible, etc.

tidied

simpler proofs of congruence rules

new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq

simpler proofs of congruence rules

new image laws

added a commment on the "ext" rule

new theorems Pow_0 and Pow_insert; renamed other Pow theorems

added rev_bexI

fixed order of multiple -m options;

fixed geometry;

tidying in conjuntion with the TISSEC paper; replaced (unit option) by a new datatype (role)

new theorem image_Union_eq

foldl_string;

renamed space2 to spacespace

tuned pretty format lookup;