equal
deleted
inserted
replaced
|
1 (* Title: HOL/ex/puzzle.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1993 TU Muenchen |
|
5 |
|
6 An question from "Bundeswettbewerb Mathematik" |
|
7 *) |
|
8 |
|
9 Puzzle = Nat + |
|
10 consts f :: "nat => nat" |
|
11 rules f_ax "f(f(n)) < f(Suc(n))" |
|
12 end |