author haftmann Wed, 01 Jan 2014 15:55:11 +0100 changeset 54892 64c2d4f8d981 parent 54891 2f4491f15fe6 child 54898 5a63324f9002
dropped obsolete references to recdef
```--- 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```
```--- 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) = (```