# HG changeset patch
# User wenzelm
# Date 1388607812 -3600
# Node ID 5a63324f9002ee7f376a1932b561e7bb63406a1d
# Parent  64c2d4f8d981085dc8890ad86c2c94680e1c8f95# Parent  b45b1b217f438f00db63bd84635369194882b219
merged

diff -r b45b1b217f43 -r 5a63324f9002 src/HOL/Isar_Examples/Fibonacci.thy
--- 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
diff -r b45b1b217f43 -r 5a63324f9002 src/HOL/Library/Code_Target_Int.thy
--- 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)"
diff -r b45b1b217f43 -r 5a63324f9002 src/HOL/Matrix_LP/SparseMatrix.thy
--- 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) = (