| Fri, 23 Aug 1996 13:12:51 +0200 |
nipkow |
Swaped two conditions in the completeness statement.
|
changeset |
files
|
| Fri, 23 Aug 1996 13:03:02 +0200 |
nipkow |
Generalized my_lemma1: (c3,s3) |--> cs3
|
changeset |
files
|
| Thu, 22 Aug 1996 12:27:01 +0200 |
paulson |
Now deepen_tac can take advantage of wrappers --
|
changeset |
files
|
| Thu, 22 Aug 1996 12:24:58 +0200 |
paulson |
Proved mem_if
|
changeset |
files
|
| Thu, 22 Aug 1996 12:24:25 +0200 |
paulson |
Proved set_of_list_subset_Cons
|
changeset |
files
|
| Thu, 22 Aug 1996 12:18:21 +0200 |
paulson |
For building the security theory as a separate database
|
changeset |
files
|
| Wed, 21 Aug 1996 13:25:27 +0200 |
paulson |
Separation of theory Event into two parts:
|
changeset |
files
|
| Wed, 21 Aug 1996 13:22:23 +0200 |
paulson |
Addition of message NS5
|
changeset |
files
|
| Wed, 21 Aug 1996 11:43:37 +0200 |
paulson |
Tidying: removing redundant args in classical reasoner calls
|
changeset |
files
|
| Wed, 21 Aug 1996 11:00:04 +0200 |
paulson |
Added le_eq_less_Suc; fixed some comments;
|
changeset |
files
|
| Tue, 20 Aug 1996 18:53:17 +0200 |
paulson |
Working version of NS, messages 1-4!
|
changeset |
files
|
| Tue, 20 Aug 1996 17:46:24 +0200 |
paulson |
Working version of NS, messages 1-3, WITH INTERLEAVING
|
changeset |
files
|
| Tue, 20 Aug 1996 12:40:17 +0200 |
paulson |
Added ref to allow suppression of error msgs
|
changeset |
files
|
| Tue, 20 Aug 1996 12:39:30 +0200 |
paulson |
New classical reasoner: warns of, and ignores, redundant rules.
|
changeset |
files
|
| Tue, 20 Aug 1996 12:36:58 +0200 |
paulson |
Addition of function set_of_list
|
changeset |
files
|
| Tue, 20 Aug 1996 12:32:16 +0200 |
paulson |
Some tidying. This brittle proof depends upon
|
changeset |
files
|
| Tue, 20 Aug 1996 12:23:13 +0200 |
paulson |
Corrected for new classical reasoner: redundant rules
|
changeset |
files
|
| Mon, 19 Aug 1996 15:35:11 +0200 |
nipkow |
updated html-link
|
changeset |
files
|
| Mon, 19 Aug 1996 13:06:30 +0200 |
paulson |
Installation of auto_tac; re-organization
|
changeset |
files
|
| Mon, 19 Aug 1996 13:03:17 +0200 |
paulson |
Tidied up the proofs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:51:39 +0200 |
paulson |
Added impOfSubs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:49:31 +0200 |
paulson |
Now less_zeroE is a Safe Elim rule
|
changeset |
files
|
| Mon, 19 Aug 1996 11:33:08 +0200 |
paulson |
Improved comment
|
changeset |
files
|
| Mon, 19 Aug 1996 11:25:04 +0200 |
paulson |
Added proof of Un_insert_right
|
changeset |
files
|
| Mon, 19 Aug 1996 11:23:25 +0200 |
paulson |
Changed precedences to remove ambiguities in r^+ notation
|
changeset |
files
|
| Mon, 19 Aug 1996 11:22:16 +0200 |
paulson |
Improved the proof of Problem 38
|
changeset |
files
|
| Mon, 19 Aug 1996 11:20:37 +0200 |
paulson |
Added a lot of basic laws, from HOL/simpdata
|
changeset |
files
|
| Mon, 19 Aug 1996 11:19:55 +0200 |
paulson |
Renaming of functions, and tidying
|
changeset |
files
|
| Mon, 19 Aug 1996 11:19:16 +0200 |
paulson |
Now starts with set_current_thy
|
changeset |
files
|
| Mon, 19 Aug 1996 11:18:36 +0200 |
paulson |
Tidied some proofs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:17:20 +0200 |
paulson |
Tidied some proofs, maybe using less_SucE
|
changeset |
files
|
| Mon, 19 Aug 1996 11:15:44 +0200 |
paulson |
Removal of less_SucE as default SE rule
|
changeset |
files
|
| Mon, 19 Aug 1996 11:12:38 +0200 |
paulson |
Renamed setOfList to set_of_list
|
changeset |
files
|
| Fri, 16 Aug 1996 11:27:10 +0200 |
oheimb |
Minor improvements of the scripts
|
changeset |
files
|
| Mon, 12 Aug 1996 16:28:15 +0200 |
paulson |
Improved (?) wording of error message
|
changeset |
files
|
| Mon, 12 Aug 1996 16:26:02 +0200 |
paulson |
Added a new section on Definitions
|
changeset |
files
|
| Mon, 12 Aug 1996 16:25:08 +0200 |
paulson |
Rewording: parameters->arguments!
|
changeset |
files
|
| Thu, 08 Aug 1996 16:28:37 +0200 |
berghofe |
Initial revision of thy_data.ML
|
changeset |
files
|
| Thu, 08 Aug 1996 16:25:53 +0200 |
berghofe |
Added function for storing default claset in theory.
|
changeset |
files
|
| Thu, 08 Aug 1996 11:45:04 +0200 |
berghofe |
Removed unnecessary Addsimps.
|
changeset |
files
|
| Thu, 08 Aug 1996 11:34:29 +0200 |
berghofe |
Simplified primrec definitions.
|
changeset |
files
|
| Fri, 02 Aug 1996 12:25:26 +0200 |
berghofe |
Classical tactics now use default claset.
|
changeset |
files
|
| Fri, 02 Aug 1996 12:16:11 +0200 |
berghofe |
Simplified primrec definitions.
|
changeset |
files
|
| Fri, 02 Aug 1996 12:14:49 +0200 |
berghofe |
Replaced prove_case_cong by Konrad Slinds optimized version.
|
changeset |
files
|
| Tue, 30 Jul 1996 18:05:22 +0200 |
berghofe |
Simplified primrec - definitions.
|
changeset |
files
|
| Tue, 30 Jul 1996 18:03:11 +0200 |
berghofe |
Now also Deepen_tac and Best_tac are used.
|
changeset |
files
|
| Tue, 30 Jul 1996 17:33:26 +0200 |
berghofe |
Classical tactics now use default claset.
|
changeset |
files
|
| Mon, 29 Jul 1996 18:31:39 +0200 |
paulson |
Works up to main theorem, then XXX...X
|
changeset |
files
|
| Mon, 29 Jul 1996 18:30:01 +0200 |
paulson |
Added two new distributive laws
|
changeset |
files
|
| Fri, 26 Jul 1996 12:31:04 +0200 |
paulson |
Addition of rev_notE
|
changeset |
files
|
| Fri, 26 Jul 1996 12:27:22 +0200 |
paulson |
Inserted spaces in error messages to improve readability
|
changeset |
files
|
| Fri, 26 Jul 1996 12:26:32 +0200 |
paulson |
Addition of contra_subsetD and rev_contra_subsetD
|
changeset |
files
|
| Fri, 26 Jul 1996 12:25:15 +0200 |
paulson |
Removal of cfast_tac
|
changeset |
files
|
| Fri, 26 Jul 1996 12:23:45 +0200 |
paulson |
Removed clash with "range" constant
|
changeset |
files
|
| Fri, 26 Jul 1996 12:20:59 +0200 |
paulson |
Redefining "range" as a macro -- new proof needed
|
changeset |
files
|
| Fri, 26 Jul 1996 12:19:46 +0200 |
paulson |
Auth proofs work up to the XXX...
|
changeset |
files
|
| Fri, 26 Jul 1996 12:18:50 +0200 |
paulson |
Proved insert_image
|
changeset |
files
|
| Fri, 26 Jul 1996 12:17:04 +0200 |
paulson |
Redefining "range" as a macro
|
changeset |
files
|
| Fri, 26 Jul 1996 12:16:17 +0200 |
paulson |
Proved bex_False
|
changeset |
files
|
| Tue, 23 Jul 1996 15:33:30 +0200 |
oheimb |
unnecessary files removed
|
changeset |
files
|
| Tue, 23 Jul 1996 13:19:27 +0200 |
paulson |
Corrected typo regarding the type of set_oracle
|
changeset |
files
|
| Mon, 22 Jul 1996 16:24:47 +0200 |
paulson |
Added insert_commute
|
changeset |
files
|
| Mon, 22 Jul 1996 16:16:51 +0200 |
paulson |
Updated BibTeX identifiers
|
changeset |
files
|
| Mon, 22 Jul 1996 16:15:45 +0200 |
paulson |
Acknowledged Martin Simons
|
changeset |
files
|
| Mon, 22 Jul 1996 16:15:00 +0200 |
paulson |
Corrected typo involving derivations
|
changeset |
files
|
| Fri, 19 Jul 1996 15:56:01 +0200 |
berghofe |
Classical tactics now use default claset.
|
changeset |
files
|
| Wed, 17 Jul 1996 17:15:54 +0200 |
pusch |
Corrected o_assoc lemma
|
changeset |
files
|
| Wed, 17 Jul 1996 17:12:33 +0200 |
pusch |
removed superfluous Park-induct rule
|
changeset |
files
|
| Wed, 17 Jul 1996 16:03:42 +0200 |
oheimb |
renamed adm_impl to adm_imp
|
changeset |
files
|
| Wed, 17 Jul 1996 15:25:50 +0200 |
paulson |
Edited in response to referees comments; new references
|
changeset |
files
|
| Wed, 17 Jul 1996 15:04:48 +0200 |
oheimb |
correction of recent typo
|
changeset |
files
|
| Tue, 16 Jul 1996 16:07:32 +0200 |
berghofe |
Added section about current claset.
|
changeset |
files
|
| Tue, 16 Jul 1996 15:49:46 +0200 |
paulson |
Put in minimal simpset to avoid excessive simplification,
Isabelle94-6
|
changeset |
files
|
| Tue, 16 Jul 1996 15:48:27 +0200 |
paulson |
corrected comment
|
changeset |
files
|
| Tue, 16 Jul 1996 15:47:07 +0200 |
paulson |
Acknowledged Stefan Berghofer for finding errors
|
changeset |
files
|
| Tue, 16 Jul 1996 15:45:36 +0200 |
paulson |
Fixed typo regarding lifting over P|P
|
changeset |
files
|
| Tue, 16 Jul 1996 15:44:31 +0200 |
paulson |
Increased revision number
|
changeset |
files
|
| Tue, 16 Jul 1996 15:44:21 +0200 |
paulson |
Tidied up; added "syntax" decl
|
changeset |
files
|
| Mon, 15 Jul 1996 14:58:28 +0200 |
paulson |
New dummy .thy files to document dependencies
|
changeset |
files
|
| Mon, 15 Jul 1996 14:54:37 +0200 |
paulson |
Uses minimal simpset (min_ss) and full_simp_tac
|
changeset |
files
|
| Mon, 15 Jul 1996 12:36:56 +0200 |
nipkow |
Documented simplification tactics which make use of the implicit simpset.
|
changeset |
files
|
| Mon, 15 Jul 1996 10:41:30 +0200 |
berghofe |
updated syntax of primrec definitions
|
changeset |
files
|
| Fri, 12 Jul 1996 20:46:32 +0200 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Fri, 12 Jul 1996 20:46:03 +0200 |
oheimb |
bug fix: Glam_ast_tr
|
changeset |
files
|
| Fri, 12 Jul 1996 20:43:12 +0200 |
oheimb |
added configuration for STEM
|
changeset |
files
|
| Fri, 12 Jul 1996 20:41:24 +0200 |
oheimb |
minor bug fix
|
changeset |
files
|
| Fri, 12 Jul 1996 17:53:15 +0200 |
berghofe |
updated syntax of primrec definitions
|
changeset |
files
|
| Fri, 12 Jul 1996 16:52:29 +0200 |
oheimb |
replaced setsolver ... by addsolver
|
changeset |
files
|
| Thu, 11 Jul 1996 15:30:22 +0200 |
paulson |
Added Msg 3; works up to Says_Server_imp_Key_newK
|
changeset |
files
|
| Thu, 11 Jul 1996 15:28:10 +0200 |
paulson |
Corrected indentation
|
changeset |
files
|
| Thu, 11 Jul 1996 15:18:57 +0200 |
paulson |
Oracles can now be strings instead of identifiers
|
changeset |
files
|
| Thu, 11 Jul 1996 15:14:41 +0200 |
paulson |
Added insert_mono
|
changeset |
files
|
| Thu, 11 Jul 1996 15:13:52 +0200 |
paulson |
Added ML reference
|
changeset |
files
|
| Thu, 11 Jul 1996 15:02:42 +0200 |
paulson |
Modified to reject certain inputs -- illustrates error handling
|
changeset |
files
|
| Thu, 11 Jul 1996 15:00:38 +0200 |
paulson |
Documentation of oracles and their syntax
|
changeset |
files
|
| Fri, 05 Jul 1996 14:22:59 +0200 |
berghofe |
Simplified syntax of primrec definitions.
|
changeset |
files
|
| Fri, 28 Jun 1996 15:30:55 +0200 |
paulson |
Removed a use of eq_cs
|
changeset |
files
|
| Fri, 28 Jun 1996 15:29:39 +0200 |
paulson |
Removed the unused eq_cs, and added some distributive laws
|
changeset |
files
|
| Fri, 28 Jun 1996 15:29:05 +0200 |
paulson |
Removed the unused rel_eq_cs
|
changeset |
files
|
| Fri, 28 Jun 1996 15:28:29 +0200 |
paulson |
Added contra_subsetD and rev_contra_subsetD
|
changeset |
files
|
| Fri, 28 Jun 1996 15:27:53 +0200 |
paulson |
Added rev_notE by analogy with rev_mp
|
changeset |
files
|
| Fri, 28 Jun 1996 15:26:39 +0200 |
paulson |
Proving safety properties of authentication protocols
|
changeset |
files
|
| Fri, 28 Jun 1996 11:19:56 +0200 |
paulson |
Updated reference to Slinds paper on TFL
|
changeset |
files
|
| Fri, 28 Jun 1996 11:16:12 +0200 |
paulson |
Now set_cs is just taken from !claset
|
changeset |
files
|
| Fri, 28 Jun 1996 11:13:07 +0200 |
paulson |
Added type-checking to rule "combination". This corrects a fault
|
changeset |
files
|
| Fri, 28 Jun 1996 11:10:32 +0200 |
paulson |
Restored warning comment
|
changeset |
files
|
| Thu, 27 Jun 1996 15:24:17 +0200 |
oheimb |
re-added when_funs to library.ML
|
changeset |
files
|
| Thu, 27 Jun 1996 15:19:50 +0200 |
oheimb |
patches for Holcfb.thy removed
|
changeset |
files
|
| Thu, 27 Jun 1996 12:53:08 +0200 |
oheimb |
removed old version of LEAST operator
|
changeset |
files
|
| Wed, 26 Jun 1996 17:50:10 +0200 |
oheimb |
repaired 8bit pragma
|
changeset |
files
|
| Wed, 26 Jun 1996 17:45:32 +0200 |
oheimb |
adapted path to 8bit package
|
changeset |
files
|
| Wed, 26 Jun 1996 17:38:34 +0200 |
oheimb |
function names in when_rews now meta-quantified
|
changeset |
files
|
| Wed, 26 Jun 1996 17:37:34 +0200 |
oheimb |
when_funs removed
|
changeset |
files
|
| Tue, 25 Jun 1996 18:01:37 +0200 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Tue, 25 Jun 1996 17:44:43 +0200 |
oheimb |
Initial revision
|
changeset |
files
|
| Tue, 25 Jun 1996 13:18:54 +0200 |
berghofe |
Changed argument order of nat_rec.
|
changeset |
files
|
| Tue, 25 Jun 1996 13:11:29 +0200 |
berghofe |
Changed argument order of nat_rec.
|
changeset |
files
|
| Fri, 21 Jun 1996 13:51:09 +0200 |
berghofe |
Replaced occurrence of fast_tac by Fast_tac .
|
changeset |
files
|
| Fri, 21 Jun 1996 13:39:08 +0200 |
berghofe |
Replaced occurrence of set_cs by claset_of "Fun" .
|
changeset |
files
|
| Fri, 21 Jun 1996 13:34:55 +0200 |
berghofe |
Added function Addss.
|
changeset |
files
|