--- a/src/HOL/Isar_Examples/Fibonacci.thy Wed Jan 01 20:14:47 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Wed Jan 01 21:23:32 2014 +0100
@@ -2,7 +2,7 @@
Author: Gertrud Bauer
Copyright 1999 Technische Universitaet Muenchen
-The Fibonacci function. Demonstrates the use of recdef. Original
+The Fibonacci function. Original
tactic script by Lawrence C Paulson.
Fibonacci numbers: proofs of laws taken from
--- a/src/HOL/Library/Code_Target_Int.thy Wed Jan 01 20:14:47 2014 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Wed Jan 01 21:23:32 2014 +0100
@@ -10,8 +10,7 @@
code_datatype int_of_integer
-lemma [code, code del]:
- "integer_of_int = integer_of_int" ..
+declare [[code drop: integer_of_int]]
lemma [code]:
"integer_of_int (int_of_integer k) = k"
@@ -57,8 +56,7 @@
"Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
by transfer simp
-lemma [code, code del]:
- "Int.sub = Int.sub" ..
+declare [[code drop: Int.sub]]
lemma [code]:
"k * l = int_of_integer (of_int k * of_int l)"
--- a/src/HOL/Matrix_LP/SparseMatrix.thy Wed Jan 01 20:14:47 2014 +0100
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy Wed Jan 01 21:23:32 2014 +0100
@@ -240,7 +240,6 @@
fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat \<Rightarrow> 'a spvec"
where
-(* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *)
"mult_spvec_spmat c [] brr = c"
| "mult_spvec_spmat c arr [] = c"
| "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (