# HG changeset patch # User paulson # Date 864998605 -7200 # Node ID d9b30c300f1e7cb361c6c24cafc2ac54bf62f8c4 # Parent 182a2b76d19e18cf8e09ed33c2a2d3cbadbfdf71 Now Divides must be the parent diff -r 182a2b76d19e -r d9b30c300f1e src/HOL/ex/Fib.thy --- a/src/HOL/ex/Fib.thy Fri May 30 15:22:19 1997 +0200 +++ b/src/HOL/ex/Fib.thy Fri May 30 15:23:25 1997 +0200 @@ -7,7 +7,7 @@ (the TFL package) *) -Fib = WF_Rel + +Fib = WF_Rel + Divides + consts fib :: "nat => nat" recdef fib "less_than"