Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
authorpaulson
Mon, 23 Oct 2006 11:18:25 +0200
changeset 21096 8f3dffd52db2
parent 21095 2c9f73fa973c
child 21097 5a59f8ff96cc
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_axioms.ML	Mon Oct 23 11:17:29 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Oct 23 11:18:25 2006 +0200
@@ -688,7 +688,7 @@
 
 fun meson_meth ths ctxt =
   Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
+    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs);
 
 val meson_method_setup =
   Method.add_methods
isabelle