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.
get_thm instead of obsolete Goals.get_thm;
authorwenzelm
Mon, 20 Jun 2005 22:13:58 +0200
changeset 16485 77ae3bfa8b76
parent 16484 eaf7bb77fed6
child 16486 1a12cdb6ee6b
get_thm instead of obsolete Goals.get_thm; improved msg;
src/HOL/arith_data.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/arith_data.ML	Mon Jun 20 22:13:57 2005 +0200
+++ b/src/HOL/arith_data.ML	Mon Jun 20 22:13:58 2005 +0200
@@ -423,7 +423,7 @@
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
     neqE = [linorder_neqE_nat,
-      Goals.get_thm (theory "Ring_and_Field") "linorder_neqE_ordered_idom"],
+      get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
     simpset = HOL_basic_ss addsimps add_rules
                    addsimprocs [ab_group_add_cancel.sum_conv, 
                                 ab_group_add_cancel.rel_conv]
@@ -464,7 +464,7 @@
 fun presburger_tac i st =
   (case ArithTheoryData.get (sign_of_thm st) of
      {presburger = SOME tac, ...} =>
-       (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
+       (warning "Simple arithmetic decision procedure failed, trying full Presburger arithmetic..."; tac i st)
    | _ => no_tac st);
 
 in
isabelle