Mon, 24 Jan 2005 18:11:06 +0100 berghofe Removed unnecessary subsignature checks to speed up rewriting.
Mon, 24 Jan 2005 18:09:29 +0100 berghofe Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
Mon, 24 Jan 2005 18:07:10 +0100 berghofe Replaced xstring by thmref.
Mon, 24 Jan 2005 17:59:48 +0100 berghofe Adapted to modified interface of PureThy.get_thm(s).
Mon, 24 Jan 2005 17:56:18 +0100 berghofe Specific theorems in a named list of theorems can now be referred to
Mon, 24 Jan 2005 16:25:36 +0100 paulson updated description of arith_tac
Mon, 24 Jan 2005 12:41:06 +0100 paulson thin_tac now works on P==>Q
Mon, 24 Jan 2005 12:40:52 +0100 paulson some rationalizing of res_inst_tac
Fri, 21 Jan 2005 18:00:18 +0100 paulson Jia Meng: delta simpsets and clasets
Fri, 21 Jan 2005 13:55:07 +0100 paulson fixed thin_tac with higher-level assumptions by removing the old code to
Fri, 21 Jan 2005 13:54:09 +0100 paulson inserted quotes preparatory to conversion
Fri, 21 Jan 2005 13:53:30 +0100 paulson fixed the treatment of demodulation and paramodulation
Fri, 21 Jan 2005 13:52:57 +0100 paulson negate_nead (???) changed to negated_asm_of_head
Fri, 21 Jan 2005 13:52:09 +0100 paulson new theorem image_eq_fold
Fri, 21 Jan 2005 13:51:39 +0100 paulson auto update
Wed, 19 Jan 2005 16:45:24 +0100 nipkow *** empty log message ***
Tue, 18 Jan 2005 14:38:20 +0100 berghofe induct_tac and case_tac no longer depend on Syntax.string_of_vname.
Tue, 18 Jan 2005 14:36:04 +0100 berghofe indexname function now parses type variables as well; changed input
Tue, 18 Jan 2005 14:34:24 +0100 berghofe Added variants of instantiation functions that operate on pairs of type
Mon, 17 Jan 2005 17:45:03 +0100 nipkow *** empty log message ***
Mon, 17 Jan 2005 15:21:40 +0100 nipkow Removed div/mod ML code because it fails for 0.
Fri, 14 Jan 2005 12:00:27 +0100 nipkow made diff_less a simp rule
Thu, 13 Jan 2005 14:56:37 +0100 berghofe Added ChangeLog
Tue, 11 Jan 2005 14:47:47 +0100 berghofe Tuned.
Tue, 11 Jan 2005 14:20:45 +0100 berghofe Option for hiding proof scripts in documents.
Tue, 11 Jan 2005 14:19:08 +0100 berghofe Added -H option for hiding proof scripts and other commands.
Tue, 11 Jan 2005 14:18:06 +0100 berghofe Swapped session.ML and isar_output.ML
Tue, 11 Jan 2005 14:16:30 +0100 berghofe Added flag for hiding proofs in documents to use_dir.
Tue, 11 Jan 2005 14:15:14 +0100 berghofe Added table of commands to be hidden in LaTeX output.
Tue, 11 Jan 2005 14:14:39 +0100 berghofe excursion_result now also passes previous state to presentation functions.
Tue, 11 Jan 2005 14:08:07 +0100 berghofe Implemented hiding of proofs and other commands.
Sat, 08 Jan 2005 09:30:16 +0100 nipkow new citation
Thu, 06 Jan 2005 05:15:26 +0100 kleing suggestions by Jeremy Siek
Thu, 06 Jan 2005 03:00:58 +0100 kleing use ISO date format
Tue, 04 Jan 2005 04:06:29 +0100 kleing added list_all_rev
Wed, 22 Dec 2004 11:36:33 +0100 nipkow [ .. (] -> [ ..< ]
Mon, 20 Dec 2004 18:25:22 +0100 nipkow *** empty log message ***
Sat, 18 Dec 2004 17:14:33 +0100 schirmer added simproc for Let
Sat, 18 Dec 2004 17:12:45 +0100 schirmer added print translation for split: split f --> %(x,y). f x y
Sat, 18 Dec 2004 17:10:49 +0100 schirmer Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
Fri, 17 Dec 2004 12:43:12 +0100 kleing Isabelle 2005 - preview
Fri, 17 Dec 2004 12:39:40 +0100 kleing sugar, not sugari. stupid vi ;-)
Fri, 17 Dec 2004 10:15:46 +0100 paulson removed two looping simplifications in SetInterval.thy; deleted the .ML file
Fri, 17 Dec 2004 10:15:10 +0100 paulson *** empty log message ***
Thu, 16 Dec 2004 14:34:23 +0100 paulson Further fix to a bug (involving equational premises) in inductive definitions
Thu, 16 Dec 2004 12:44:32 +0100 paulson fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
Thu, 16 Dec 2004 04:19:20 +0100 kleing LaTeXsugar
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
Wed, 15 Dec 2004 10:19:19 +0100 paulson *** empty log message ***
Wed, 15 Dec 2004 10:19:01 +0100 paulson removal of HOL_Lemmas
Tue, 14 Dec 2004 14:53:02 +0100 paulson converted Relation_Power to new-style theory
Tue, 14 Dec 2004 10:45:16 +0100 paulson new and stronger lemmas and improved simplification for finite sets
Tue, 14 Dec 2004 10:40:07 +0100 paulson tidied; removed references to HOL theories
Mon, 13 Dec 2004 18:41:49 +0100 nipkow added find_rewrites
Mon, 13 Dec 2004 17:44:52 +0100 nipkow *** empty log message ***
Mon, 13 Dec 2004 17:07:47 +0100 nipkow added find_rewrites
Mon, 13 Dec 2004 15:06:59 +0100 paulson removal of NatArith.ML and Product_Type.ML
Mon, 13 Dec 2004 14:31:02 +0100 aspinall Fix pgmlsymbolson/off.
Sun, 12 Dec 2004 16:25:47 +0100 nipkow REorganized Finite_Set
Fri, 10 Dec 2004 22:33:16 +0100 aspinall Support PGIP <whitespace>, <dostep>, <doitem> elements as input
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip