tuned;

--- a/NEWS	Wed Sep 26 22:28:00 2007 +0200
+++ b/NEWS	Wed Sep 26 22:38:11 2007 +0200
@@ -413,6 +413,9 @@
 
   definition "K x _ = x"
 
+  inductive conj for A B
+  where "A ==> B ==> conj A B"
+
 * Pure: command 'print_abbrevs' prints all constant abbreviations of
 the current context.  Print mode "no_abbrevs" prevents inversion of
 abbreviations on output.