Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Sat, 19 Feb 2005 18:44:34 +0100 dixon lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
Fri, 18 Feb 2005 15:20:27 +0100 nipkow continued eliminating sumr
Fri, 18 Feb 2005 11:48:53 +0100 nipkow starting to get rid of sumr
Fri, 18 Feb 2005 11:48:42 +0100 nipkow tuning
Wed, 16 Feb 2005 19:00:49 +0100 nipkow *** empty log message ***
Tue, 15 Feb 2005 16:56:15 +0100 berghofe refine now provides specific cases "goal1" ... "goaln" for addressing
Mon, 14 Feb 2005 10:24:58 +0100 paulson simplified a proof
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Fri, 11 Feb 2005 18:51:00 +0100 berghofe Fully qualified refl and trans to avoid confusion with theorems
Fri, 11 Feb 2005 17:11:24 +0100 berghofe Optimized present_tokens to produce fewer newlines when hiding proofs.
Fri, 11 Feb 2005 10:03:41 +0100 ballarin New reference Toplevel.debug for verbose printing of exns.
Fri, 11 Feb 2005 04:36:22 +0100 kleing update from Larry
Thu, 10 Feb 2005 19:14:35 +0100 nipkow some stuff is now redundant.
Thu, 10 Feb 2005 18:51:54 +0100 nipkow HOL.order -> Orderings.order due to restructering
Thu, 10 Feb 2005 18:51:12 +0100 nipkow Moved oderings from HOL into the new Orderings.thy
Thu, 10 Feb 2005 17:09:15 +0100 berghofe Added paper by M. Takahashi.
Thu, 10 Feb 2005 17:08:45 +0100 berghofe Added proof of eta-postponement theorem (using parallel eta-reduction).
Thu, 10 Feb 2005 16:03:18 +0100 paulson non-inductive fold1Set proofs
Thu, 10 Feb 2005 13:01:46 +0100 paulson simplified a key lemma for foldSet
Thu, 10 Feb 2005 12:06:40 +0100 ballarin Toplevel.debug for debugging in Isar.
Thu, 10 Feb 2005 11:19:03 +0100 berghofe Fixed bug in select_thm.
Thu, 10 Feb 2005 10:43:57 +0100 berghofe Subscripts for theorem lists now start at 1.
Thu, 10 Feb 2005 08:25:22 +0100 kleing mention authors are acknowledged for isabelle-lemmas
Thu, 10 Feb 2005 08:21:40 +0100 kleing more preview
Thu, 10 Feb 2005 07:47:06 +0100 kleing pointer to isabelle-lemmas submission list
Wed, 09 Feb 2005 18:51:02 +0100 nipkow added lattice_locales
Wed, 09 Feb 2005 18:50:09 +0100 nipkow Extracted generic lattice stuff to new Lattice_Locales.thy
Wed, 09 Feb 2005 18:49:29 +0100 nipkow New
Wed, 09 Feb 2005 18:32:28 +0100 paulson new foldSet proofs
Wed, 09 Feb 2005 12:08:46 +0100 paulson revised fold1 proofs
Wed, 09 Feb 2005 10:17:09 +0100 paulson revised fold1 proofs
Tue, 08 Feb 2005 18:32:34 +0100 nipkow cvs merge problem fixed
Tue, 08 Feb 2005 15:11:30 +0100 paulson new treatment of fold1
Tue, 08 Feb 2005 09:46:00 +0100 nipkow Fixed lattice defns
Mon, 07 Feb 2005 18:20:46 +0100 nipkow *** empty log message ***
Mon, 07 Feb 2005 08:02:49 +0100 nipkow fixed latex problems by including bigsqcap
Mon, 07 Feb 2005 08:02:14 +0100 nipkow fixed latex problems
Sun, 06 Feb 2005 13:12:32 +0100 paulson fixed mac line
Sat, 05 Feb 2005 19:24:11 +0100 nipkow Added Lattice locale
Fri, 04 Feb 2005 18:35:46 +0100 paulson clausification and proof reconstruction
Fri, 04 Feb 2005 18:34:34 +0100 paulson comment
Fri, 04 Feb 2005 17:14:42 +0100 nipkow Added semi-lattice locales and reorganized fold1 lemmas
Thu, 03 Feb 2005 16:45:59 +0100 nipkow added find_rewrites
Thu, 03 Feb 2005 16:06:19 +0100 paulson new treatment of demodulation in proof reconstruction
Thu, 03 Feb 2005 04:09:52 +0100 kleing don't generate latex for LaTeXsugar and OptionalSugar
Thu, 03 Feb 2005 03:56:11 +0100 kleing removed sugar.sty (obsolete for devel version)
Thu, 03 Feb 2005 03:34:44 +0100 kleing not needed any more by LaTeXSugar
Thu, 03 Feb 2005 03:33:55 +0100 kleing Document now applies to devel version (and Isabelle 2005)
Wed, 02 Feb 2005 18:20:31 +0100 berghofe Replaced application of subst by simplesubst in proof of app_Var_NF
Wed, 02 Feb 2005 18:19:43 +0100 berghofe Replaced application of subst by simplesubst in proof of rev_induct
Wed, 02 Feb 2005 18:06:25 +0100 paulson tidying of some subst/simplesubst proofs
Wed, 02 Feb 2005 18:06:00 +0100 paulson generalization and tidying
Wed, 02 Feb 2005 15:43:04 +0100 paulson improved handling of chained facts
Wed, 02 Feb 2005 10:16:33 +0100 nipkow Max_le -> Max_ge
Wed, 02 Feb 2005 09:15:40 +0100 nipkow fold and fol1 changes
Wed, 02 Feb 2005 08:53:03 +0100 nipkow added [simp]
Wed, 02 Feb 2005 08:45:14 +0100 kleing link to PG FAQ for start up problem
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Sun, 30 Jan 2005 20:48:50 +0100 nipkow renamed a few vars, added a lemma
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip