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->
Tue, 07 May 1996 18:15:51 +0200 paulson Unfolding of arbitrarily nested tuples in induction rules
Tue, 07 May 1996 18:14:39 +0200 paulson Now split_all_tac works for i>1 !
Tue, 07 May 1996 09:58:12 +0200 berghofe Added function claset_of.
Tue, 07 May 1996 09:53:20 +0200 berghofe Added function for storing default claset in theory.
Tue, 07 May 1996 09:46:25 +0200 berghofe Added functions for default claset.
Mon, 06 May 1996 15:22:33 +0200 berghofe Replaced split_tac by split_inside_tac.
Mon, 06 May 1996 15:21:05 +0200 berghofe Added split_inside_tac.
Mon, 06 May 1996 15:19:50 +0200 berghofe Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
Mon, 06 May 1996 10:44:43 +0200 paulson Updated timings; more theorems can be proved
Mon, 06 May 1996 10:39:54 +0200 paulson Now mentions but does not load mesontest2.ML
Fri, 03 May 1996 17:40:05 +0200 paulson updated comments for handling derivations
Fri, 03 May 1996 17:35:13 +0200 paulson Extra examples for safe_meson_tac
Thu, 02 May 1996 12:00:37 +0200 paulson Restored a proof of Pelletier #38 -- mysteriously deleted
Thu, 02 May 1996 10:20:15 +0200 nipkow Added note on types.
Wed, 01 May 1996 13:55:20 +0200 paulson Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
Wed, 01 May 1996 13:48:31 +0200 paulson New cancellation and monotonicity laws, about
Wed, 01 May 1996 13:47:21 +0200 paulson Two new "obvious" examples
Wed, 01 May 1996 10:43:16 +0200 paulson Provides merge_cs to support default clasets
Wed, 01 May 1996 10:38:14 +0200 paulson Simplified KG's proofs
Wed, 01 May 1996 10:37:07 +0200 paulson New lemma inspired by KG
Wed, 01 May 1996 10:35:06 +0200 paulson tidied some proofs
Tue, 30 Apr 1996 17:32:29 +0200 nipkow Added an equivalence proof which avoids the use of -n->
Tue, 30 Apr 1996 17:30:54 +0200 nipkow Added backwards rtrancl_induct and special versions for pairs.
Tue, 30 Apr 1996 13:40:32 +0200 clasohm changed ident_no_colon so that it forbids postfix "=", too
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip