Thu, 06 Jun 1996 13:13:18 +0200 paulson Quotes now optional around inductive set
Tue, 04 Jun 1996 12:49:04 +0200 paulson Tidied some proofs
Mon, 03 Jun 1996 17:10:56 +0200 berghofe best_tac, deepen_tac and safe_tac now also use default claset.
Mon, 03 Jun 1996 11:44:44 +0200 paulson Shortened some proofs
Mon, 03 Jun 1996 11:43:55 +0200 paulson Added a new theorem, UN_Int_subset
Mon, 03 Jun 1996 11:41:26 +0200 paulson Used 2 instead of Suc(Suc 0)
Mon, 03 Jun 1996 11:41:00 +0200 paulson Shortened a proof
Fri, 31 May 1996 20:25:59 +0200 oheimb adapted use of monofun_cfun_arg
Fri, 31 May 1996 20:14:42 +0200 oheimb adapted proof of flat_codom
Fri, 31 May 1996 19:55:19 +0200 oheimb introduced forgotten bind_thm calls
Fri, 31 May 1996 19:47:23 +0200 oheimb adapted some proofs for new simplifier
Fri, 31 May 1996 19:34:40 +0200 oheimb renamed le_0 to le_0_eq, to avoid confusion with le0,
Fri, 31 May 1996 19:12:00 +0200 oheimb moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
Thu, 30 May 1996 13:31:29 +0200 nipkow Smaller logo
Thu, 30 May 1996 13:29:52 +0200 nipkow Regrouped logo
Wed, 29 May 1996 13:53:39 +0200 nipkow Added logo
Wed, 29 May 1996 13:47:43 +0200 nipkow An Isabelle logo
Wed, 29 May 1996 13:34:17 +0200 nipkow Replaced setsolver by addsolver
Wed, 29 May 1996 12:03:32 +0200 nipkow Added addsolver
Tue, 28 May 1996 11:19:16 +0200 paulson Simplified proof of deduction theorem
Tue, 28 May 1996 11:16:38 +0200 paulson Corrected a comment in #34
Fri, 24 May 1996 12:27:04 +0200 berghofe Rules pred_0, pred_Suc etc. are now stored in theorem database.
Fri, 24 May 1996 11:48:18 +0200 nipkow Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
Fri, 24 May 1996 11:46:40 +0200 nipkow Removed junk introduced by a cvs merge.
Fri, 24 May 1996 11:42:04 +0200 paulson Augmented comment about conversion to clauses
Thu, 23 May 1996 15:17:23 +0200 berghofe expanded TABs
Thu, 23 May 1996 15:16:12 +0200 berghofe equalityI is now added to default claset
Thu, 23 May 1996 15:15:20 +0200 berghofe Removed equalityI from some proofs (because it is now included
Thu, 23 May 1996 14:37:06 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Wed, 22 May 1996 18:32:37 +0200 nipkow Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
Wed, 22 May 1996 17:30:16 +0200 nipkow Added ex_imp
Wed, 22 May 1996 17:11:54 +0200 nipkow Added the second half of the W/I correspondence.
Wed, 22 May 1996 16:54:16 +0200 nipkow Added swap_prems_rl
Tue, 21 May 1996 13:42:53 +0200 berghofe Added additional parent theory equalities because some proofs in
Tue, 21 May 1996 13:39:31 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Tue, 21 May 1996 10:52:26 +0200 nipkow Corrected comment wrt I
Tue, 21 May 1996 10:50:40 +0200 nipkow Updated url.
Mon, 20 May 1996 18:41:55 +0200 nipkow Added thm I_complete_wrt_W to I.
Mon, 20 May 1996 10:11:30 +0200 berghofe replaced result() by qed "sorted_insort" in last proof
Fri, 17 May 1996 16:22:23 +0200 nipkow Added missing default clause | top_const _ = None;
Fri, 17 May 1996 16:08:06 +0200 nipkow Added if_image_distrib.
Fri, 17 May 1996 12:24:47 +0200 nipkow Had to rename params because variable names in an induction rule changed.
Fri, 17 May 1996 12:23:44 +0200 nipkow Moved split_rule et al from ind_syntax.ML to Prod.ML.
Wed, 15 May 1996 13:51:15 +0200 paulson Deleted spurious line break
Fri, 10 May 1996 17:41:10 +0200 paulson Corrected and augmented timings
Fri, 10 May 1996 17:03:17 +0200 paulson Updated for new form of induction rules
Thu, 09 May 1996 11:46:32 +0200 paulson Updated for new form of induction rules
Thu, 09 May 1996 11:45:53 +0200 paulson Removed special syntax for -a-> and nested tuples to left
Thu, 09 May 1996 11:45:00 +0200 paulson Updated for new form of induction rules
Thu, 09 May 1996 11:43:44 +0200 paulson Added prune_params_tac to improve readability of subgoals
Wed, 08 May 1996 18:01:54 +0200 paulson moved ap_split to cartprod.ML
Wed, 08 May 1996 17:59:21 +0200 paulson Modified to use new functor signatures
Wed, 08 May 1996 17:57:05 +0200 paulson Predicates are now uncurried in both induction rules,
Wed, 08 May 1996 17:54:07 +0200 paulson Uses new ap_split from cartprod module
Wed, 08 May 1996 17:52:52 +0200 paulson New functor for operating on the two forms of Cartesian product
Wed, 08 May 1996 17:49:16 +0200 paulson Added new name cartprod
Wed, 08 May 1996 17:43:23 +0200 paulson Updated for new form of induction rules
Wed, 08 May 1996 16:10:32 +0200 paulson Updated for new form of induction rules
Tue, 07 May 1996 18:19:13 +0200 paulson Updated for new form of induction rules
Tue, 07 May 1996 18:17:52 +0200 paulson Removal of special syntax for -a-> and -b->
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip