isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Fri, 28 Oct 2005 02:25:57 +0200 Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.

changeset

mengj [Fri, 28 Oct 2005 02:25:57 +0200] rev 18000

Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.

Fri, 28 Oct 2005 02:24:58 +0200 Added several functions to the signature.

changeset

mengj [Fri, 28 Oct 2005 02:24:58 +0200] rev 17999

Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.

Fri, 28 Oct 2005 02:23:49 +0200 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.

changeset

mengj [Fri, 28 Oct 2005 02:23:49 +0200] rev 17998

A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.

Thu, 27 Oct 2005 18:25:33 +0200 sorted lemma lists

changeset

paulson [Thu, 27 Oct 2005 18:25:33 +0200] rev 17997

sorted lemma lists

Thu, 27 Oct 2005 13:59:06 +0200 * HOL: alternative iff syntax;

changeset

wenzelm [Thu, 27 Oct 2005 13:59:06 +0200] rev 17996

* HOL: alternative iff syntax;

Thu, 27 Oct 2005 13:54:43 +0200 consts: monomorphic;

changeset

wenzelm [Thu, 27 Oct 2005 13:54:43 +0200] rev 17995

consts: monomorphic;