author | wenzelm |
Sat, 03 Nov 2001 01:35:11 +0100 | |
changeset 12024 | b3661262541e |
parent 9243 | 22b460a0b676 |
child 12431 | 07ec657249e5 |
permissions | -rw-r--r-- |
(* Title: HOL/IMP/Examples.thy ID: $Id$ Author: David von Oheimb, TUM Copyright 2000 TUM *) Examples = Natural + defs (* bring up the deferred definition for update *) update_def "update == fun_upd" constdefs factorial :: loc => loc => com "factorial a b == b :== (%s. 1); WHILE (%s. s a ~= 0) DO (b :== (%s. s b * s a); a :== (%s. s a - 1))" end