author | oheimb |
Tue, 04 Jul 2000 14:04:56 +0200 | |
changeset 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