# HG changeset patch # User paulson # Date 1091792164 -7200 # Node ID e2bd080c7975214efca8896abc1ddbe926c4773a # Parent b860e444c1db4cb93052c78a9cce2ef4b842b11f make_clauses now meta diff -r b860e444c1db -r e2bd080c7975 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Aug 06 13:35:44 2004 +0200 +++ b/src/HOL/Tools/meson.ML Fri Aug 06 13:36:04 2004 +0200 @@ -371,7 +371,7 @@ let val n = nprems_of th in if 1 <= i andalso i <= n then Thm.permute_prems (i-1) 1 th - else raise THM("make_last", i, [th]) + else raise THM("select_literal", i, [th]) end; (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing @@ -398,8 +398,9 @@ REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); -(*Top-level conversion to clauses (disjunctions). Each clause has - leading !!-bound universal variables, to express generality.*) +(*Top-level conversion to meta-level clauses. Each clause has + leading !!-bound universal variables, to express generality. To get + disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*) val make_clauses_tac = SUBGOAL (fn (prop,_) => @@ -407,12 +408,13 @@ in EVERY1 [METAHYPS (fn hyps => - (cut_rules_tac (map forall_intr_vars (make_clauses hyps)) 1)), + (cut_rules_tac + (map forall_intr_vars + (make_meta_clauses (make_clauses hyps))) 1)), REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); - (** proof method setup **) local @@ -438,7 +440,7 @@ ("skolemize", Method.no_args skolemize_meth, "Skolemization into existential quantifiers"), ("make_clauses", Method.no_args make_clauses_meth, - "Conversion to !!-quantified disjunctions")]]; + "Conversion to !!-quantified meta-level clauses")]]; end;