Thu, 21 Oct 2004 19:21:32 +0200 Fix <closetheory>
aspinall [Thu, 21 Oct 2004 19:21:32 +0200] rev 15253
Fix <closetheory>
Tue, 19 Oct 2004 22:45:20 +0200 Replaced PolyML specific print function by Display.print_thm(s)
berghofe [Tue, 19 Oct 2004 22:45:20 +0200] rev 15252
Replaced PolyML specific print function by Display.print_thm(s)
Tue, 19 Oct 2004 18:18:45 +0200 converted some induct_tac to induct
paulson [Tue, 19 Oct 2004 18:18:45 +0200] rev 15251
converted some induct_tac to induct
Mon, 18 Oct 2004 13:40:45 +0200 added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon [Mon, 18 Oct 2004 13:40:45 +0200] rev 15250
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
Mon, 18 Oct 2004 11:43:40 +0200 Replaced list of bound variables in simpset by maximal index of bound
berghofe [Mon, 18 Oct 2004 11:43:40 +0200] rev 15249
Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).
Fri, 15 Oct 2004 18:49:16 +0200 record_split_simp_tac now can get simp rules as parameter
schirmer [Fri, 15 Oct 2004 18:49:16 +0200] rev 15248
record_split_simp_tac now can get simp rules as parameter
Fri, 15 Oct 2004 18:16:11 +0200 update
nipkow [Fri, 15 Oct 2004 18:16:11 +0200] rev 15247
update
Fri, 15 Oct 2004 18:16:03 +0200 added and renamed
nipkow [Fri, 15 Oct 2004 18:16:03 +0200] rev 15246
added and renamed
Thu, 14 Oct 2004 12:18:52 +0200 Added a few lemmas
nipkow [Thu, 14 Oct 2004 12:18:52 +0200] rev 15245
Added a few lemmas
Wed, 13 Oct 2004 07:40:13 +0200 mod becuase of chnage in induct
nipkow [Wed, 13 Oct 2004 07:40:13 +0200] rev 15244
mod becuase of chnage in induct
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip