| author | wenzelm |
| Thu, 15 Nov 2001 18:20:13 +0100 | |
| changeset 12207 | 4dff931b852f |
| parent 9243 | 22b460a0b676 |
| child 12431 | 07ec657249e5 |
| permissions | -rw-r--r-- |
| 9243 | 1 |
(* Title: HOL/IMP/Examples.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb, TUM |
|
4 |
Copyright 2000 TUM |
|
5 |
*) |
|
6 |
||
7 |
Examples = Natural + |
|
8 |
||
9 |
defs (* bring up the deferred definition for update *) |
|
10 |
||
11 |
update_def "update == fun_upd" |
|
12 |
||
13 |
constdefs |
|
14 |
||
15 |
factorial :: loc => loc => com |
|
16 |
"factorial a b == b :== (%s. 1); |
|
17 |
WHILE (%s. s a ~= 0) DO |
|
18 |
(b :== (%s. s b * s a); a :== (%s. s a - 1))" |
|
19 |
||
20 |
end |