src/HOL/Tools/meson.ML
changeset 15965 f422f8283491
parent 15946 94e5f157ab09
child 15998 bc916036cf84
     1.1 --- a/src/HOL/Tools/meson.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -317,7 +317,8 @@
     1.4  fun make_nnf th = th |> simplify nnf_ss
     1.5                       |> check_no_bool |> make_nnf1
     1.6  
     1.7 -(*Pull existential quantifiers (Skolemization)*)
     1.8 +(*Pull existential quantifiers to front. This accomplishes Skolemization for
     1.9 +  clauses that arise from a subgoal.*)
    1.10  fun skolemize th =
    1.11    if not (has_consts ["Ex"] (prop_of th)) then th
    1.12    else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.13 @@ -331,7 +332,7 @@
    1.14  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.15    The resulting clauses are HOL disjunctions.*)
    1.16  fun make_clauses ths =
    1.17 -   (  sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    1.18 +    (sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    1.19  
    1.20  
    1.21  (*Convert a list of clauses to (contrapositive) Horn clauses*)