skalberg [Mon, 21 Jul 2003 17:27:23 +0200] rev 14122
Added handling of meta implication and meta quantification.
skalberg [Mon, 21 Jul 2003 16:19:34 +0200] rev 14121
Added handling of free variables (provided they are of sort HOL.type).
paulson [Mon, 21 Jul 2003 13:02:07 +0200] rev 14120
Tidied some examples
skalberg [Mon, 21 Jul 2003 10:58:16 +0200] rev 14119
Added the specification command.
skalberg [Mon, 21 Jul 2003 08:53:56 +0200] rev 14118
Changed bstring argument to xstring.
skalberg [Mon, 21 Jul 2003 08:52:06 +0200] rev 14117
*** empty log message ***
skalberg [Sat, 19 Jul 2003 17:35:15 +0200] rev 14116
Added optional theorem names for the constant definitions added during
specification.
skalberg [Thu, 17 Jul 2003 15:23:20 +0200] rev 14115
Added package for definition by specification.
paulson [Wed, 16 Jul 2003 12:09:41 +0200] rev 14114
tidying
paulson [Tue, 15 Jul 2003 15:20:54 +0200] rev 14113
Fixing a simproc bug
paulson [Tue, 15 Jul 2003 15:12:22 +0200] rev 14112
tidying
nipkow [Tue, 15 Jul 2003 08:25:20 +0200] rev 14111
Some new thm (ex_map_conv?)