Mon, 15 Jul 1996 14:58:28 +0200 paulson New dummy .thy files to document dependencies
Mon, 15 Jul 1996 14:54:37 +0200 paulson Uses minimal simpset (min_ss) and full_simp_tac
Mon, 15 Jul 1996 12:36:56 +0200 nipkow Documented simplification tactics which make use of the implicit simpset.
Mon, 15 Jul 1996 10:41:30 +0200 berghofe updated syntax of primrec definitions
Fri, 12 Jul 1996 20:46:32 +0200 oheimb *** empty log message ***
Fri, 12 Jul 1996 20:46:03 +0200 oheimb bug fix: Glam_ast_tr
Fri, 12 Jul 1996 20:43:12 +0200 oheimb added configuration for STEM
Fri, 12 Jul 1996 20:41:24 +0200 oheimb minor bug fix
Fri, 12 Jul 1996 17:53:15 +0200 berghofe updated syntax of primrec definitions
Fri, 12 Jul 1996 16:52:29 +0200 oheimb replaced setsolver ... by addsolver
Thu, 11 Jul 1996 15:30:22 +0200 paulson Added Msg 3; works up to Says_Server_imp_Key_newK
Thu, 11 Jul 1996 15:28:10 +0200 paulson Corrected indentation
Thu, 11 Jul 1996 15:18:57 +0200 paulson Oracles can now be strings instead of identifiers
Thu, 11 Jul 1996 15:14:41 +0200 paulson Added insert_mono
Thu, 11 Jul 1996 15:13:52 +0200 paulson Added ML reference
Thu, 11 Jul 1996 15:02:42 +0200 paulson Modified to reject certain inputs -- illustrates error handling
Thu, 11 Jul 1996 15:00:38 +0200 paulson Documentation of oracles and their syntax
Fri, 05 Jul 1996 14:22:59 +0200 berghofe Simplified syntax of primrec definitions.
Fri, 28 Jun 1996 15:30:55 +0200 paulson Removed a use of eq_cs
Fri, 28 Jun 1996 15:29:39 +0200 paulson Removed the unused eq_cs, and added some distributive laws
Fri, 28 Jun 1996 15:29:05 +0200 paulson Removed the unused rel_eq_cs
Fri, 28 Jun 1996 15:28:29 +0200 paulson Added contra_subsetD and rev_contra_subsetD
Fri, 28 Jun 1996 15:27:53 +0200 paulson Added rev_notE by analogy with rev_mp
Fri, 28 Jun 1996 15:26:39 +0200 paulson Proving safety properties of authentication protocols
Fri, 28 Jun 1996 11:19:56 +0200 paulson Updated reference to Slinds paper on TFL
Fri, 28 Jun 1996 11:16:12 +0200 paulson Now set_cs is just taken from !claset
Fri, 28 Jun 1996 11:13:07 +0200 paulson Added type-checking to rule "combination". This corrects a fault
Fri, 28 Jun 1996 11:10:32 +0200 paulson Restored warning comment
Thu, 27 Jun 1996 15:24:17 +0200 oheimb re-added when_funs to library.ML
Thu, 27 Jun 1996 15:19:50 +0200 oheimb patches for Holcfb.thy removed
Thu, 27 Jun 1996 12:53:08 +0200 oheimb removed old version of LEAST operator
Wed, 26 Jun 1996 17:50:10 +0200 oheimb repaired 8bit pragma
Wed, 26 Jun 1996 17:45:32 +0200 oheimb adapted path to 8bit package
Wed, 26 Jun 1996 17:38:34 +0200 oheimb function names in when_rews now meta-quantified
Wed, 26 Jun 1996 17:37:34 +0200 oheimb when_funs removed
Tue, 25 Jun 1996 18:01:37 +0200 oheimb *** empty log message ***
Tue, 25 Jun 1996 17:44:43 +0200 oheimb Initial revision
Tue, 25 Jun 1996 13:18:54 +0200 berghofe Changed argument order of nat_rec.
Tue, 25 Jun 1996 13:11:29 +0200 berghofe Changed argument order of nat_rec.
Fri, 21 Jun 1996 13:51:09 +0200 berghofe Replaced occurrence of fast_tac by Fast_tac .
Fri, 21 Jun 1996 13:39:08 +0200 berghofe Replaced occurrence of set_cs by claset_of "Fun" .
Fri, 21 Jun 1996 13:34:55 +0200 berghofe Added function Addss.
Fri, 21 Jun 1996 12:18:50 +0200 berghofe Classical tactics now use default claset.
Fri, 21 Jun 1996 11:57:00 +0200 oheimb minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
Thu, 20 Jun 1996 10:27:29 +0200 paulson Restored Addsimps [Suc_le_lessD], as it cannot be added
Thu, 20 Jun 1996 10:26:13 +0200 paulson Corrected comment
Tue, 18 Jun 1996 16:38:48 +0200 paulson New rewrites for vacuous quantification
Tue, 18 Jun 1996 16:37:47 +0200 paulson Addition of setOfList
Tue, 18 Jun 1996 16:36:04 +0200 paulson Addition of Safe_step_tac
Tue, 18 Jun 1996 16:27:04 +0200 paulson Translation infixes <->, etc., no longer available at top-level
Tue, 18 Jun 1996 16:20:30 +0200 paulson Addition of setOfList
Tue, 18 Jun 1996 16:18:44 +0200 paulson Removal of list_all
Tue, 18 Jun 1996 16:17:38 +0200 paulson Translation infixes <->, etc., no longer available at top-level
Mon, 17 Jun 1996 16:51:47 +0200 paulson Inserted comment about problem 43
Mon, 17 Jun 1996 16:51:11 +0200 paulson Removed quantification over lists
Mon, 17 Jun 1996 16:50:38 +0200 paulson Now exports Delrules
Mon, 17 Jun 1996 16:50:08 +0200 paulson Converted to use constdefs instead of defs
Fri, 14 Jun 1996 12:37:21 +0200 paulson Explicitly included add_mult_distrib & add_mult_distrib2
Fri, 14 Jun 1996 12:34:56 +0200 paulson New example of greatest common divisor
Fri, 14 Jun 1996 12:32:08 +0200 paulson Added Primes to list of theories in target ex
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip