haftmann [Fri, 28 Oct 2005 16:35:40 +0200] rev 18011
cleaned up nth, nth_update, nth_map and nth_string functions
berghofe [Fri, 28 Oct 2005 13:52:57 +0200] rev 18010
Removed legacy prove_goalw_cterm command.
paulson [Fri, 28 Oct 2005 12:22:34 +0200] rev 18009
got rid of obsolete prove_goalw_cterm
haftmann [Fri, 28 Oct 2005 09:36:19 +0200] rev 18008
swapped add_datatype result
haftmann [Fri, 28 Oct 2005 09:35:04 +0200] rev 18007
removed obfuscating PStrStrTab
haftmann [Fri, 28 Oct 2005 08:40:55 +0200] rev 18006
reachable - abandoned foldl_map in favor of fold_map
mengj [Fri, 28 Oct 2005 02:30:53 +0200] rev 18005
Added Tools/res_hol_clause.ML
mengj [Fri, 28 Oct 2005 02:30:12 +0200] rev 18004
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
mengj [Fri, 28 Oct 2005 02:29:01 +0200] rev 18003
Added "writeln_strs" to the signature
mengj [Fri, 28 Oct 2005 02:28:20 +0200] rev 18002
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.