src/HOL/IMP/Examples.thy
changeset 9243 22b460a0b676
child 12431 07ec657249e5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Examples.thy	Tue Jul 04 14:04:56 2000 +0200
     1.3 @@ -0,0 +1,20 @@
     1.4 +(*  Title:      HOL/IMP/Examples.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb, TUM
     1.7 +    Copyright   2000 TUM
     1.8 +*)
     1.9 +
    1.10 +Examples = Natural +
    1.11 +
    1.12 +defs (* bring up the deferred definition for update *)
    1.13 +
    1.14 + update_def "update == fun_upd"
    1.15 +
    1.16 +constdefs
    1.17 +  
    1.18 +  factorial :: loc => loc => com
    1.19 + "factorial a b == b :== (%s. 1);
    1.20 +               WHILE (%s. s a ~= 0) DO
    1.21 +                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    1.22 +  
    1.23 +end