1996-11-01 paulson 1996-11-01 New version with simpler disambiguation in YM3, Oops message, and no encryption in YM2
1996-11-01 paulson 1996-11-01 New, purely illustrative result Crypt_synth_analz
1996-11-01 paulson 1996-11-01 Proof of antisym_less_lift now simpler and more robust
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max
1996-11-01 paulson 1996-11-01 Changes tabs found in .thy files to spaces
1996-11-01 paulson 1996-11-01 Replaced "sum" (only usage?) by foldl op+
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max
1996-11-01 paulson 1996-11-01 maxidx_of_typs replaces max o map maxidx_of_typ
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max nodup_Vars now updates maxidx
1996-11-01 paulson 1996-11-01 maxidx_of_typs replaces max o map maxidx_of_typ Now uses Int.max instead of max
1996-11-01 paulson 1996-11-01 asm_rewrite_goal_tac now calls SELECT_GOAL. Replaced min by Int.min
1996-11-01 paulson 1996-11-01 Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
1996-11-01 paulson 1996-11-01 Replaced min by Int.min
1996-11-01 paulson 1996-11-01 Deleted Olist constructor. Replaced minidx by "above" function
1996-11-01 paulson 1996-11-01 Now defines structure Int
1996-10-30 paulson 1996-10-30 Changed some mem calls to mem_int for greater efficiency (not that it could matter)
1996-10-30 paulson 1996-10-30 Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
1996-10-30 paulson 1996-10-30 Changed some mem calls to mem_string for greater efficiency (not that it could matter)
1996-10-30 paulson 1996-10-30 Minor updates
1996-10-30 paulson 1996-10-30 Updated references
1996-10-28 paulson 1996-10-28 Minor corrections
1996-10-28 nipkow 1996-10-28 Renamed and shuffled a few thms.
1996-10-28 paulson 1996-10-28 Simplified proofs
1996-10-28 paulson 1996-10-28 Tidied up a big mess in UN_parts_sees_Says
1996-10-28 paulson 1996-10-28 Changing from the Reveal to the Oops rule
1996-10-27 nipkow 1996-10-27 Simplifid proofs.
1996-10-25 nipkow 1996-10-25 Added (? x. t=x) = True
1996-10-24 paulson 1996-10-24 Documents the use of negative arguments to choplev and prlev
1996-10-24 paulson 1996-10-24 Changed comment to illustrate use of pathname
1996-10-24 paulson 1996-10-24 Allowing negative levels (as offsets) in prlev and choplev
1996-10-24 paulson 1996-10-24 New Oops message, with Server as source to ensure correct nonces
1996-10-24 paulson 1996-10-24 New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
1996-10-24 paulson 1996-10-24 Two new protocol variants
1996-10-24 paulson 1996-10-24 Moved ex_strip_tac to the common part
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy
1996-10-24 paulson 1996-10-24 Handles pathnames in ISABELLECOMP
1996-10-21 paulson 1996-10-21 Mentions the possibility of pathnames in ISABELLECOMP;
1996-10-21 paulson 1996-10-21 Creates a bigger main window
1996-10-21 paulson 1996-10-21 ISABELLECOMP may now have a leading pathname
1996-10-21 nipkow 1996-10-21 Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
1996-10-21 nipkow 1996-10-21 Added trans_tac (see Provers/nat_transitive.ML)
1996-10-21 nipkow 1996-10-21 Solves simple arithmetic goals.
1996-10-18 paulson 1996-10-18 Subst as modified by Konrad Slind
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL
1996-10-18 paulson 1996-10-18 New version of Yahalom, as recommended on p 259 of BAN paper
1996-10-18 paulson 1996-10-18 Addition of Reveal message
1996-10-18 paulson 1996-10-18 Deleted obsolete rewrites (they are now in HOL/simpdata)
1996-10-18 paulson 1996-10-18 Reveal -> Revl
1996-10-18 paulson 1996-10-18 The new proof of the lemma for new_nonces_not_seen is faster
1996-10-18 paulson 1996-10-18 Generaly tidying up
1996-10-18 paulson 1996-10-18 Important correction to comment
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac; tidied proofs
1996-10-18 paulson 1996-10-18 Tidied up the proof of A_trust_NS4
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac
1996-10-18 paulson 1996-10-18 Moving the CPUtimer declaration into cond_timeit should prevent the problems that caused exn TIME to be raised
1996-10-18 paulson 1996-10-18 Now checks that $LISTEN is set
1996-10-16 nipkow 1996-10-16 Defined pred using nat_case rather than nat_rec. Added expand_nat_case
1996-10-15 oheimb 1996-10-15 corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)
1996-10-15 oheimb 1996-10-15 bound o_apply theorem to thy
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles