diff -r 428efffe8599 -r b50b8c0eec01 src/FOL/cladata.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/cladata.ML Fri Jan 03 15:01:55 1997 +0100 @@ -0,0 +1,51 @@ +(* Title: FOL/cladata.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1996 University of Cambridge + +Setting up the classical reasoner +*) + + +(** Applying HypsubstFun to generate hyp_subst_tac **) +section "Classical Reasoner"; + +(*** Applying ClassicalFun to create a classical prover ***) +structure Classical_Data = + struct + val sizef = size_of_thm + val mp = mp + val not_elim = notE + val classical = classical + val hyp_subst_tacs=[hyp_subst_tac] + end; + +structure Cla = ClassicalFun(Classical_Data); +open Cla; + +(*Propositional rules + -- iffCE might seem better, but in the examples in ex/cla + run about 7% slower than with iffE*) +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] + addSEs [conjE,disjE,impCE,FalseE,iffE]; + +(*Quantifier rules*) +val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] + addSEs [exE,ex1E] addEs [allE]; + + +exception CS_DATA of claset; + +let fun merge [] = CS_DATA empty_cs + | merge cs = let val cs = map (fn CS_DATA x => x) cs; + in CS_DATA (foldl merge_cs (hd cs, tl cs)) end; + + fun put (CS_DATA cs) = claset := cs; + + fun get () = CS_DATA (!claset); +in add_thydata "FOL" + ("claset", ThyMethods {merge = merge, put = put, get = get}) +end; + +claset := FOL_cs; +