berghofe [Tue, 28 Aug 2007 18:03:16 +0200] rev 24452
- theorem(_i) now also takes "interactive" flag as argument
- added theorem hook
berghofe [Tue, 28 Aug 2007 18:01:37 +0200] rev 24451
Specification.theorem now also takes "interactive" flag as argument.
nipkow [Tue, 28 Aug 2007 16:33:52 +0200] rev 24450
Commented out non-standard paragraph formatting.
nipkow [Tue, 28 Aug 2007 15:34:15 +0200] rev 24449
added (code) lemmas for setsum and foldl
wenzelm [Tue, 28 Aug 2007 11:51:27 +0200] rev 24448
replaced 'sorry' by unproven;
wenzelm [Tue, 28 Aug 2007 11:25:32 +0200] rev 24447
do not touch quick_and_dirty;
wenzelm [Tue, 28 Aug 2007 11:25:31 +0200] rev 24446
norm_absolute: CRITICAL;
wenzelm [Tue, 28 Aug 2007 11:25:30 +0200] rev 24445
tuned load order -- minimizes modules before Secure;
wenzelm [Tue, 28 Aug 2007 11:25:29 +0200] rev 24444
induct: proper separation of initial and terminal step;
avoid unspecific prems;
huffman [Tue, 28 Aug 2007 03:58:37 +0200] rev 24443
move WordExamples to Examples directory
huffman [Tue, 28 Aug 2007 03:56:24 +0200] rev 24442
HOL-Word-Examples
huffman [Tue, 28 Aug 2007 03:49:18 +0200] rev 24441
Word Examples directory
kleing [Tue, 28 Aug 2007 00:18:10 +0200] rev 24440
add parallel sessions for atbroy99 and macbroy6
wenzelm [Mon, 27 Aug 2007 17:34:55 +0200] rev 24439
HOL_USEDIR_OPTIONS: no special -M setting (now works with multithreaded);
nipkow [Mon, 27 Aug 2007 14:19:38 +0200] rev 24438
Added infinite_descent
haftmann [Mon, 27 Aug 2007 11:34:19 +0200] rev 24437
updated keywords
haftmann [Mon, 27 Aug 2007 11:34:18 +0200] rev 24436
added code_props
haftmann [Mon, 27 Aug 2007 11:34:17 +0200] rev 24435
introduces params_of_sort
haftmann [Mon, 27 Aug 2007 11:34:16 +0200] rev 24434
added simple definition scheme
haftmann [Mon, 27 Aug 2007 11:34:14 +0200] rev 24433
added explicit equation for equality of nested environments
haftmann [Mon, 27 Aug 2007 08:31:01 +0200] rev 24432
circumvented infix problem
nipkow [Sun, 26 Aug 2007 21:28:08 +0200] rev 24431
tuned linear arith (once again) with ring_distribs
haftmann [Sun, 26 Aug 2007 14:37:18 +0200] rev 24430
made SML/NJ happy
kleing [Sun, 26 Aug 2007 01:19:20 +0200] rev 24429
described 'rotated' attribute
haftmann [Sat, 25 Aug 2007 09:22:22 +0200] rev 24428
made SML/NJ happy
paulson [Fri, 24 Aug 2007 14:21:33 +0200] rev 24427
revised blacklisting for ATP linkup
paulson [Fri, 24 Aug 2007 14:17:54 +0200] rev 24426
new derived rule: incr_type_indexes
paulson [Fri, 24 Aug 2007 14:16:44 +0200] rev 24425
Returning both a "one-line" proof and a structured proof
paulson [Fri, 24 Aug 2007 14:15:58 +0200] rev 24424
Reconstruction bug fix
haftmann [Fri, 24 Aug 2007 14:14:20 +0200] rev 24423
overloaded definitions accompanied by explicit constants