*** empty log message ***

*** empty log message ***

*** empty log message ***

TODO

proper order of order_less_asym';

cleanup, tuned

converted many HOL/Auth theories to Isar scripts

symlinks to ../../../HOL/Auth. Fingers crossed...

Protocols chapter

back to Unix format...

security protocol chapter

security protocol refs

new theorem Fake_parts_insert_in_Un

extra display

*** empty log message ***

lexicographic product of two relations: updated HOL.tex Also automatic updates by xemacs

Isar hint

thm output: Attrib.local_thmss;

tuned

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

quantifier instantiation

the one-point rule for bounded quantifiers

generalization of 1 point rules for ALL

*** empty log message ***

misc tidying; changing the predicate isSymKey to the set symKeys

Got rid of is_dfa

MicroJava/BV dependencies incomplete

fixed bug in tactic for ball 1 point simproc

Vos

simplified proofs

simplified proofs

I forgot a few bases cases for the 1-point rules...

shortening and streamlining of proofs

added simproc for bounded quantifiers

added one point simprocs for bounded quantifiers

new theorem analz_Decrypt'

new theorem analz_isSymKey_Decrypt

some X-symbols

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

translations: a tweak

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

minor tuning

*** empty log message ***

*** empty log message ***

*** empty log message ***

arith_tac now copes with propositional reasoning as well.

expanded abbrevs

added strange 'b y' syntax

*** empty log message ***

*** empty log message ***

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

a few basic X-symbols

conversion of Message.thy to Isar format

*** empty log message ***

conversion of Message.thy to Isar format

streamlined a proof

auto-update

*** empty log message ***

Some X-symbols for <notin>, <noteq>, <forall>, <exists> Streamlining of Yahalom proofs Removal of redundant proofs

kildall now via while and therefore executable!

minor tweaks to speed the proofs

minor fixes

renamed addaltern to addafter, addSaltern to addSafter

removed performance leak for split_conv_tac (and corresponding safe wrapper)

subst method and a new section on rule, rule_tac, etc

removed unused constant

removed unused function

a PROPER tidy-up

recoded function iter with the help of the while-combinator.

revisions in response to comments by Tobias

revisions in response to comments by Tobias

added split_conv_tac (also to claset()) as an optimization

made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL

simplified proofs for splitI and splitD, added splitD' added split_conv_tac (also to claset()) as an optimization made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL

made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL

corrected comments on addbefore and addSbefore

added same_fstI

simplified definition of wrapper bspec

added image_cong to default congs of recdef

added add_arith (just as hint by now)

added rearrange_prems

debugging: replaced gen_all by forall_elim_vars_safe

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

fixed the obvious errors Tobias found

Least_def now refers to LeastM

for the change to LEAST

Blast bug fix made old proof too slow

Blast bug fix: now always duplicates when applying a haz rule, whether or not new variables are added. Can now prove theorems such as these: val prems = Goal "[|P==>Q; P==>~Q|] ==> ~P"; by (blast_tac (claset() addDs prems) 1); val prems = Goal "[|Q==>P; ~Q==>P|] ==> P"; by (blast_tac (claset() addIs prems) 1);

Blast bug fix made old proof too slow

Streamlining for the bug fix in Blast. MPair_parts now built in using AddSEs, throughout.

*** empty log message ***

*** empty log message ***

*** empty log message ***

tuned;

eliminate get_def;

tuned;

Ord.thy/.ML converted to Isar

moved inv_image to Relation nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML added wf_linord_ex_has_least,LeastM_nat_lemma,LeastM_natI,LeastM_nat_le

supressed some warnings on identical proofstate moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least from Nat.ML to Wellfounded_Recursion.ML added wellorder axclass

Ord.thy/.ML converted to Isar added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy moved Least_equality from Nat.ML to Ord.thy added LeastM operator

moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least from Nat.ML to Wellfounded_Recursion.ML moved Least_equality from Nat.ML to Ord.thy moved wf_less from Nat.ML to NatDef.ML added wellorder axclass nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy

simplified proof of Least_mono

added wellorder axclass

moved inv_image to Relation

moved wf_less from Nat.ML to NatDef.ML

added nat as instance of new wellorder axclass

Ord.thy/.ML converted to Isar

added trial proof

improved subst_RS

added missiong word

*** empty log message ***

index mod syntax;

tuned;

isatool install -k;

handle KDE version 1 or 2;

isatool install handles KDE version 1 or 2;

removed whitespace

supressed some warnings on identical proofstate

adhoc script for creating complete Isabelle dist pages;

imp_cong2 -> imp_cong

new function get_overloads

updated the unicity proof

tidying

not_bad_tac is obsolete

a new theorem from Bryan Ford

added support for AddXIs, AddXEs, AddXDs

tuned;

tuned;

tuned;

\remarksfalse;

tuned;

swapped Fleuriot and Paulson

create dist packages;

partial conversion to Isar script style in HOL/Auth removes some .ML files

partial conversion to Isar script style in HOL/Auth removes some .ML files

partial conversion to Isar script style simplified unicity proofs

tuned;

tuned;

support \<subseteq> syntax in classes/classrel/axclass/instance;

\<subseteq> syntax for classes/classrel/axclass/instance;

\<subseteq>;

added "xsymbols" syntax for "=?=";

more robust selection of calculational rules;

tuned trans rules;

updated;

tuned;

Changes to HOL/Algebra: - Axclasses consolidated (axiom one_not_zero). - Now uses summation operator setsum; SUM has been removed. - Priority of infix assoc changed to 50, in accordance to dvd.

Definition of setsum (sort constraint) relaxed to {zero, plus}.

Updates to HOL/Algebra: - axclasses consolidated (lemma one_not_zero) - summation operator SUM removed, now uses setsum Use of setsum made it necessary to relax sort constraint in its definition to {zero, plus}.

tuned;

lower priority for forw_subst;

tuned;

not used any more (all Isar style)

removed MicroJava/Digest.thy

tuned for 99-2 release

unsymbolized; tuned;

tuned;

improved;

solved non-initialization problems; improvements using prefer

various revisions in response to comments from Tobias

val get_goal: state -> context * (thm list * thm);

4.0 version;

snapshot of a new version

new theorem Transset_iff_Union_subset

tuned

improved;

polyml multiplatform setup;

tuned

tuned;

improved document (added headers etc)

tuned

improvements concerning instantiations etc.

disable non-existant chapters

tuned;

fixed version string;

polyml-3.x.ML vs polyml-4.0.ML;

renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default);

tuned;

example Proof General settings;

document setup;

converted to new-style;

moved theory Perm to HOL/Library;

added no_document

tuned

added Permutation;

moved from Induct/ to Library/

updated

added no_document;

updated split_format;

* no_document ML operator temporarily disables LaTeX document generation;

HOL-NumberTheory: converted to new-style format and proper document setup;

tuned msg;

tuned;

Induct: converted some theories to new-style format;

fixed syntax of 'split_format';

use fgrep;

HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old format may recovered via ML function complete_split_rule or attribute 'split_rule (complete)';

commutation theory, ported by Sidi Ehmety

updated;

simplified 'split_format' syntax;

'split_format' attribute;

tuned;

module setup; use hidden internal_split constants;

use hol_simplify;

use hol_rewrite_cterm;

added hol_simplify, hol_rewrite_cterm;

split = split_conv (for compatibility);

added hidden internal_split constant; tuned;

isatool convert;

new theorem fib_mult_eq_setsum

little bugfixes; added induct_thm_tac

moved to Product_Type_lemmas.ML

added translations for bind_thm and val

converted to Isar, simplifying recursion on class hierarchy

converted to Isar therory, adding attributes complete_split and split_format

converted to new-style theories;

updated

ext_classrel: certify_class;

comment

tuned

tuned;

added "numerals" theorems;