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.
dropped two inline directives
authorhaftmann
Mon, 18 Dec 2006 08:21:30 +0100
changeset 21874 aa350df2372c
parent 21873 62d2416728f5
child 21875 5df10a17644e
dropped two inline directives
src/HOL/Library/EfficientNat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/EfficientNat.thy	Mon Dec 18 08:21:29 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Mon Dec 18 08:21:30 2006 +0100
@@ -64,13 +64,13 @@
   by (simp add: nat_of_int_def)
 lemma [code func]: "Suc n = n + 1"
   by simp
-lemma [code, code inline]: "m + n = nat (int m + int n)"
+lemma [code]: "m + n = nat (int m + int n)"
   by arith
 lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
   by (simp add: nat_of_int_def)
 lemma [code, code inline]: "m - n = nat (int m - int n)"
   by arith
-lemma [code, code inline]: "m * n = nat (int m * int n)"
+lemma [code]: "m * n = nat (int m * int n)"
   unfolding zmult_int by simp
 lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
 proof -
isabelle