src/CCL/ROOT.ML

(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)

(*  Title:      CCL/ROOT.ML
    ID:         $Id$
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Classical Computational Logic based on First-Order Logic.
*)

set eta_contract;

(* CCL - a computational logic for an untyped functional language *)
(*                       with evaluation to weak head-normal form *)

use_thys ["Wfd", "Fix"];