isabelle: src/HOL/ex/Fib.thy@dbf2d9b3d6c8 (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
3494 f7ac2d1e2051 Fixed comments paulson parents: 3375 diff changeset	6	The Fibonacci function. Demonstrates the use of recdef.
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	7	*)
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	8
6481 dbf2d9b3d6c8 recdef requires theory Recdef; wenzelm parents: 4809 diff changeset	9	Fib = Divides + Primes +
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	10
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	11	consts fib :: "nat => nat"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	12	recdef fib "less_than"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	13	"fib 0 = 0"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	14	"fib 1 = 1"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	15	"fib (Suc(Suc x)) = (fib x + fib (Suc x))"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	16
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	17	end

author	wenzelm
	Thu, 22 Apr 1999 13:04:23 +0200
changeset 6481	dbf2d9b3d6c8
parent 4809	595f905cc348
child 8658	3cf533397c5a
permissions	-rw-r--r--