# HG changeset patch
# User haftmann
# Date 1388588111 -3600
# Node ID 64c2d4f8d981085dc8890ad86c2c94680e1c8f95
# Parent  2f4491f15fe6ed03cb9354862fd1b401cd2840ce
dropped obsolete references to recdef

diff -r 2f4491f15fe6 -r 64c2d4f8d981 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Wed Jan 01 11:35:21 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Wed Jan 01 15:55:11 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 2f4491f15fe6 -r 64c2d4f8d981 src/HOL/Matrix_LP/SparseMatrix.thy
--- a/src/HOL/Matrix_LP/SparseMatrix.thy	Wed Jan 01 11:35:21 2014 +0100
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Wed Jan 01 15:55:11 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) = (