make_clauses now meta
authorpaulson
Fri Aug 06 13:36:04 2004 +0200 (2004-08-06)
changeset 15118e2bd080c7975
parent 15117 b860e444c1db
child 15119 e5f167042c1d
make_clauses now meta
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 06 13:35:44 2004 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 06 13:36:04 2004 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4    let val n = nprems_of th 
     1.5    in  if 1 <= i andalso i <= n 
     1.6        then Thm.permute_prems (i-1) 1 th
     1.7 -      else raise THM("make_last", i, [th])
     1.8 +      else raise THM("select_literal", i, [th])
     1.9    end;
    1.10  
    1.11  (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
    1.12 @@ -398,8 +398,9 @@
    1.13  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.14       end);
    1.15  
    1.16 -(*Top-level conversion to clauses (disjunctions). Each clause has  
    1.17 -  leading !!-bound universal variables, to express generality.*)
    1.18 +(*Top-level conversion to meta-level clauses. Each clause has  
    1.19 +  leading !!-bound universal variables, to express generality. To get 
    1.20 +  disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
    1.21  val make_clauses_tac = 
    1.22    SUBGOAL
    1.23      (fn (prop,_) =>
    1.24 @@ -407,12 +408,13 @@
    1.25       in EVERY1 
    1.26  	 [METAHYPS
    1.27  	    (fn hyps => 
    1.28 -              (cut_rules_tac (map forall_intr_vars (make_clauses hyps)) 1)),
    1.29 +              (cut_rules_tac
    1.30 +                (map forall_intr_vars 
    1.31 +                  (make_meta_clauses (make_clauses hyps))) 1)),
    1.32  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.33       end);
    1.34  
    1.35  
    1.36 -
    1.37  (** proof method setup **)
    1.38  
    1.39  local
    1.40 @@ -438,7 +440,7 @@
    1.41     ("skolemize", Method.no_args skolemize_meth, 
    1.42      "Skolemization into existential quantifiers"),
    1.43     ("make_clauses", Method.no_args make_clauses_meth, 
    1.44 -    "Conversion to !!-quantified disjunctions")]];
    1.45 +    "Conversion to !!-quantified meta-level clauses")]];
    1.46  
    1.47  end;
    1.48