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.
Some error messages have been eliminated as suggested by Tobias Nipkow
authorchaieb
Mon, 06 Jun 2005 13:43:39 +0200
changeset 16299 872ad146bb14
parent 16298 8435be7188cb
child 16300 a4e163c7ed9c
Some error messages have been eliminated as suggested by Tobias Nipkow
src/HOL/Integ/cooper_dec.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/cooper_dec.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/cooper_dec.ML	Mon Jun 06 13:30:21 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Mon Jun 06 13:43:39 2005 +0200
@@ -198,9 +198,9 @@
         if is_numeral s' then (linear_cmul (dest_numeral s') t') 
         else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
  
-         else (warning "lint: apparent nonlinearity"; raise COOPER)
+         else raise COOPER
          end 
-  |_ =>  error ("COOPER:lint: unknown term  \n");
+  |_ =>  raise COOPER;
    
  
  
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 06 13:30:21 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 06 13:43:39 2005 +0200
@@ -198,9 +198,9 @@
         if is_numeral s' then (linear_cmul (dest_numeral s') t') 
         else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
  
-         else (warning "lint: apparent nonlinearity"; raise COOPER)
+         else raise COOPER
          end 
-  |_ =>  error ("COOPER:lint: unknown term  \n");
+  |_ =>  raise COOPER;
isabelle