huffman [Tue, 08 Mar 2005 00:32:10 +0100] rev 15593
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:28:46 +0100] rev 15592
removed Cprod3_lemma1 and Cprod3_lemma2
huffman [Tue, 08 Mar 2005 00:18:22 +0100] rev 15591
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:15:01 +0100] rev 15590
added subsection headings, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:11:49 +0100] rev 15589
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:00:49 +0100] rev 15588
arranged for document generation, cleaned up some proofs
huffman [Mon, 07 Mar 2005 23:54:01 +0100] rev 15587
added subsections and text for document generation
huffman [Mon, 07 Mar 2005 23:30:06 +0100] rev 15586
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
webertj [Mon, 07 Mar 2005 19:41:04 +0100] rev 15585
HTML 4.01 Transitional conformity
webertj [Mon, 07 Mar 2005 19:30:53 +0100] rev 15584
refute_params: default value itself=1 added (for type classes)
webertj [Mon, 07 Mar 2005 19:25:13 +0100] rev 15583
HTML 4.01 Transitional conformity
webertj [Mon, 07 Mar 2005 19:17:07 +0100] rev 15582
HTML 4.01 Transitional conformity
paulson [Mon, 07 Mar 2005 18:40:36 +0100] rev 15581
now checks for higher-order vars
obua [Mon, 07 Mar 2005 18:19:55 +0100] rev 15580
Cleaning up HOL/Matrix
paulson [Mon, 07 Mar 2005 16:55:36 +0100] rev 15579
Tools/meson.ML: signature, structure and "open" rather than "local"
huffman [Fri, 04 Mar 2005 23:25:06 +0100] rev 15578
add header
huffman [Fri, 04 Mar 2005 23:23:47 +0100] rev 15577
fix headers
huffman [Fri, 04 Mar 2005 23:12:36 +0100] rev 15576
converted to new-style theories, and combined numbered files
huffman [Fri, 04 Mar 2005 18:53:46 +0100] rev 15575
document generation for HOLCF
skalberg [Fri, 04 Mar 2005 15:07:34 +0100] rev 15574
Removed practically all references to Library.foldr.
paulson [Fri, 04 Mar 2005 11:44:26 +0100] rev 15573
new first_order test
paulson [Fri, 04 Mar 2005 10:58:04 +0100] rev 15572
removed dead code
webertj [Thu, 03 Mar 2005 17:22:46 +0100] rev 15571
interpreter for Finite_Set.Finites added
skalberg [Thu, 03 Mar 2005 12:43:01 +0100] rev 15570
Move towards standard functions.
nipkow [Thu, 03 Mar 2005 09:22:35 +0100] rev 15569
fixed proof
huffman [Thu, 03 Mar 2005 01:37:32 +0100] rev 15568
converted to new-style theory
huffman [Thu, 03 Mar 2005 00:42:04 +0100] rev 15567
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:58:02 +0100] rev 15566
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:28:17 +0100] rev 15565
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:15:16 +0100] rev 15564
converted to new-style theory
huffman [Wed, 02 Mar 2005 22:57:08 +0100] rev 15563
converted to new-style theory
huffman [Wed, 02 Mar 2005 22:30:00 +0100] rev 15562
converted to new-style theory
nipkow [Wed, 02 Mar 2005 12:06:15 +0100] rev 15561
another reorganization of setsums and intervals
dixon [Wed, 02 Mar 2005 10:33:10 +0100] rev 15560
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
paulson [Wed, 02 Mar 2005 10:21:17 +0100] rev 15559
obscured the e-mail address lcp@cl
paulson [Wed, 02 Mar 2005 10:02:21 +0100] rev 15558
new lemmas int_diff_cases
huffman [Wed, 02 Mar 2005 00:56:41 +0100] rev 15557
eliminated deps for removed files
huffman [Wed, 02 Mar 2005 00:55:12 +0100] rev 15556
merged into Discrete.thy
huffman [Wed, 02 Mar 2005 00:54:06 +0100] rev 15555
converted to new-style theory
nipkow [Tue, 01 Mar 2005 18:48:52 +0100] rev 15554
integrated Jeremy's FiniteLib
kleing [Tue, 01 Mar 2005 05:44:13 +0100] rev 15553
spider dogding
obua [Mon, 28 Feb 2005 18:29:55 +0100] rev 15552
added setsum_diff1' which holds in more general cases than setsum_diff1
paulson [Mon, 28 Feb 2005 13:10:36 +0100] rev 15551
unfold theorems for trancl and rtrancl
dixon [Sun, 27 Feb 2005 00:00:40 +0100] rev 15550
lucas - added more comments and an extra type to clarify the code.
berghofe [Wed, 23 Feb 2005 15:19:00 +0100] rev 15549
Modified node_trans to avoid duplication of signature stamps
when undoing.
webertj [Wed, 23 Feb 2005 15:00:03 +0100] rev 15548
exception SAME removed
webertj [Wed, 23 Feb 2005 14:04:53 +0100] rev 15547
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
nipkow [Wed, 23 Feb 2005 10:23:22 +0100] rev 15546
suminf -> \<Sum>
dixon [Tue, 22 Feb 2005 18:42:22 +0100] rev 15545
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
paulson [Tue, 22 Feb 2005 13:05:47 +0100] rev 15544
removed redundant lemmas and simprules
nipkow [Tue, 22 Feb 2005 10:54:30 +0100] rev 15543
more setsum tuning
nipkow [Mon, 21 Feb 2005 19:23:46 +0100] rev 15542
more fine tuniung
nipkow [Mon, 21 Feb 2005 18:04:28 +0100] rev 15541
fixed proof
nipkow [Mon, 21 Feb 2005 15:57:45 +0100] rev 15540
removed superfluous setsum_constant
nipkow [Mon, 21 Feb 2005 15:04:10 +0100] rev 15539
comprehensive cleanup, replacing sumr by setsum
dixon [Sat, 19 Feb 2005 18:44:34 +0100] rev 15538
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.
nipkow [Fri, 18 Feb 2005 15:20:27 +0100] rev 15537
continued eliminating sumr
nipkow [Fri, 18 Feb 2005 11:48:53 +0100] rev 15536
starting to get rid of sumr
nipkow [Fri, 18 Feb 2005 11:48:42 +0100] rev 15535
tuning
nipkow [Wed, 16 Feb 2005 19:00:49 +0100] rev 15534
*** empty log message ***
berghofe [Tue, 15 Feb 2005 16:56:15 +0100] rev 15533
refine now provides specific cases "goal1" ... "goaln" for addressing
subgoals of a proof state.
paulson [Mon, 14 Feb 2005 10:24:58 +0100] rev 15532
simplified a proof
skalberg [Sun, 13 Feb 2005 17:15:14 +0100] rev 15531
Deleted Library.option type.
berghofe [Fri, 11 Feb 2005 18:51:00 +0100] rev 15530
Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.
berghofe [Fri, 11 Feb 2005 17:11:24 +0100] rev 15529
Optimized present_tokens to produce fewer newlines when hiding proofs.
ballarin [Fri, 11 Feb 2005 10:03:41 +0100] rev 15528
New reference Toplevel.debug for verbose printing of exns.
kleing [Fri, 11 Feb 2005 04:36:22 +0100] rev 15527
update from Larry
nipkow [Thu, 10 Feb 2005 19:14:35 +0100] rev 15526
some stuff is now redundant.
nipkow [Thu, 10 Feb 2005 18:51:54 +0100] rev 15525
HOL.order -> Orderings.order due to restructering
nipkow [Thu, 10 Feb 2005 18:51:12 +0100] rev 15524
Moved oderings from HOL into the new Orderings.thy
berghofe [Thu, 10 Feb 2005 17:09:15 +0100] rev 15523
Added paper by M. Takahashi.
berghofe [Thu, 10 Feb 2005 17:08:45 +0100] rev 15522
Added proof of eta-postponement theorem (using parallel eta-reduction).
paulson [Thu, 10 Feb 2005 16:03:18 +0100] rev 15521
non-inductive fold1Set proofs
paulson [Thu, 10 Feb 2005 13:01:46 +0100] rev 15520
simplified a key lemma for foldSet
ballarin [Thu, 10 Feb 2005 12:06:40 +0100] rev 15519
Toplevel.debug for debugging in Isar.
berghofe [Thu, 10 Feb 2005 11:19:03 +0100] rev 15518
Fixed bug in select_thm.
berghofe [Thu, 10 Feb 2005 10:43:57 +0100] rev 15517
Subscripts for theorem lists now start at 1.
kleing [Thu, 10 Feb 2005 08:25:22 +0100] rev 15516
mention authors are acknowledged for isabelle-lemmas
kleing [Thu, 10 Feb 2005 08:21:40 +0100] rev 15515
more preview
kleing [Thu, 10 Feb 2005 07:47:06 +0100] rev 15514
pointer to isabelle-lemmas submission list
nipkow [Wed, 09 Feb 2005 18:51:02 +0100] rev 15513
added lattice_locales
nipkow [Wed, 09 Feb 2005 18:50:09 +0100] rev 15512
Extracted generic lattice stuff to new Lattice_Locales.thy
nipkow [Wed, 09 Feb 2005 18:49:29 +0100] rev 15511
New
paulson [Wed, 09 Feb 2005 18:32:28 +0100] rev 15510
new foldSet proofs
paulson [Wed, 09 Feb 2005 12:08:46 +0100] rev 15509
revised fold1 proofs
paulson [Wed, 09 Feb 2005 10:17:09 +0100] rev 15508
revised fold1 proofs
nipkow [Tue, 08 Feb 2005 18:32:34 +0100] rev 15507
cvs merge problem fixed
paulson [Tue, 08 Feb 2005 15:11:30 +0100] rev 15506
new treatment of fold1
nipkow [Tue, 08 Feb 2005 09:46:00 +0100] rev 15505
Fixed lattice defns
nipkow [Mon, 07 Feb 2005 18:20:46 +0100] rev 15504
*** empty log message ***
nipkow [Mon, 07 Feb 2005 08:02:49 +0100] rev 15503
fixed latex problems by including bigsqcap
nipkow [Mon, 07 Feb 2005 08:02:14 +0100] rev 15502
fixed latex problems
paulson [Sun, 06 Feb 2005 13:12:32 +0100] rev 15501
fixed mac line
nipkow [Sat, 05 Feb 2005 19:24:11 +0100] rev 15500
Added Lattice locale
paulson [Fri, 04 Feb 2005 18:35:46 +0100] rev 15499
clausification and proof reconstruction
paulson [Fri, 04 Feb 2005 18:34:34 +0100] rev 15498
comment
nipkow [Fri, 04 Feb 2005 17:14:42 +0100] rev 15497
Added semi-lattice locales and reorganized fold1 lemmas
nipkow [Thu, 03 Feb 2005 16:45:59 +0100] rev 15496
added find_rewrites
paulson [Thu, 03 Feb 2005 16:06:19 +0100] rev 15495
new treatment of demodulation in proof reconstruction
kleing [Thu, 03 Feb 2005 04:09:52 +0100] rev 15494
don't generate latex for LaTeXsugar and OptionalSugar
kleing [Thu, 03 Feb 2005 03:56:11 +0100] rev 15493
removed sugar.sty (obsolete for devel version)
kleing [Thu, 03 Feb 2005 03:34:44 +0100] rev 15492
not needed any more by LaTeXSugar
kleing [Thu, 03 Feb 2005 03:33:55 +0100] rev 15491
Document now applies to devel version (and Isabelle 2005)
berghofe [Wed, 02 Feb 2005 18:20:31 +0100] rev 15490
Replaced application of subst by simplesubst in proof of app_Var_NF
to avoid problems with program extraction.
berghofe [Wed, 02 Feb 2005 18:19:43 +0100] rev 15489
Replaced application of subst by simplesubst in proof of rev_induct
to avoid problems with program extraction.
paulson [Wed, 02 Feb 2005 18:06:25 +0100] rev 15488
tidying of some subst/simplesubst proofs
paulson [Wed, 02 Feb 2005 18:06:00 +0100] rev 15487
generalization and tidying
paulson [Wed, 02 Feb 2005 15:43:04 +0100] rev 15486
improved handling of chained facts
nipkow [Wed, 02 Feb 2005 10:16:33 +0100] rev 15485
Max_le -> Max_ge
nipkow [Wed, 02 Feb 2005 09:15:40 +0100] rev 15484
fold and fol1 changes
nipkow [Wed, 02 Feb 2005 08:53:03 +0100] rev 15483
added [simp]
kleing [Wed, 02 Feb 2005 08:45:14 +0100] rev 15482
link to PG FAQ for start up problem