isabelle: src/HOL/ex/Fib.thy@e85c24717cad (annotated)

3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	1	(* Title: ex/Fib
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	2	ID: $Id$
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	4	Copyright 1997 University of Cambridge
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	5
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	6	Fibonacci numbers and other simple examples of recursive definitions
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	7	(the TFL package)
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	8	*)
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	9
3375 d9b30c300f1e Now Divides must be the parent paulson parents: 3300 diff changeset	10	Fib = WF_Rel + Divides +
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	11
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	12	consts fib :: "nat => nat"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	13	recdef fib "less_than"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	14	"fib 0 = 0"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	15	"fib 1 = 1"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	16	"fib (Suc(Suc x)) = (fib x + fib (Suc x))"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	17
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	18	end

author	nipkow
	Thu, 26 Jun 1997 13:20:50 +0200
changeset 3465	e85c24717cad
parent 3375	d9b30c300f1e
child 3494	f7ac2d1e2051
permissions	-rw-r--r--