Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IntDiv.thy
changeset 31998 2c7a24f74db9
parent 31734 a4a79836d07b
child 32010 cb1a1c94b4cd
child 32069 6d28bbd33e2c 
--- a/src/HOL/IntDiv.thy	Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:54:04 2009 +0200
@@ -36,7 +36,7 @@
 
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
-  [code inline]: "negateSnd = apsnd uminus"
+  [code_inline]: "negateSnd = apsnd uminus"
 
 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b
isabelle