Wed, 22 Oct 2003 10:51:30 +0200 recursion
paulson [Wed, 22 Oct 2003 10:51:30 +0200] rev 14243
recursion
Tue, 21 Oct 2003 11:09:23 +0200 Added access to the mk_rews field (and friends).
skalberg [Tue, 21 Oct 2003 11:09:23 +0200] rev 14242
Added access to the mk_rews field (and friends).
Fri, 17 Oct 2003 11:04:36 +0200 Prevent recdef from looping when the inductio rule is simplified
paulson [Fri, 17 Oct 2003 11:04:36 +0200] rev 14241
Prevent recdef from looping when the inductio rule is simplified
Fri, 17 Oct 2003 11:03:48 +0200 improved tracing
paulson [Fri, 17 Oct 2003 11:03:48 +0200] rev 14240
improved tracing
Thu, 16 Oct 2003 12:13:43 +0200 partial conversion to Isar scripts
paulson [Thu, 16 Oct 2003 12:13:43 +0200] rev 14239
partial conversion to Isar scripts
Thu, 16 Oct 2003 10:32:36 +0200 improved presentation
paulson [Thu, 16 Oct 2003 10:32:36 +0200] rev 14238
improved presentation
Thu, 16 Oct 2003 10:32:06 +0200 line-breaks; rewording
paulson [Thu, 16 Oct 2003 10:32:06 +0200] rev 14237
line-breaks; rewording
Thu, 16 Oct 2003 10:31:40 +0200 partial conversion to Isar scripts
paulson [Thu, 16 Oct 2003 10:31:40 +0200] rev 14236
partial conversion to Isar scripts
Wed, 15 Oct 2003 11:02:28 +0200 Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe [Wed, 15 Oct 2003 11:02:28 +0200] rev 14235
Fixed bug in mk_ind_def that caused the inductive definition package to crash in cases where the declaration of a constant and its definition were located in different theory files.
Wed, 15 Oct 2003 07:03:43 +0200 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
kleing [Wed, 15 Oct 2003 07:03:43 +0200] rev 14234
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip