doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
changeset 30242 aea5d7fa7ef5
parent 30241 3a1aef73b2b2
parent 30236 e70dae49dc57
child 30244 48543b307e99
child 30251 7aec011818e0
child 30257 06b2d7f9f64b
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Wed Mar 04 11:05:02 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,24 +0,0 @@
     1.4 -structure Nat = 
     1.5 -struct
     1.6 -
     1.7 -datatype nat = Suc of nat | Zero_nat;
     1.8 -
     1.9 -end; (*struct Nat*)
    1.10 -
    1.11 -structure Codegen = 
    1.12 -struct
    1.13 -
    1.14 -type 'a null = {null : 'a};
    1.15 -fun null (A_:'a null) = #null A_;
    1.16 -
    1.17 -fun head A_ (x :: xs) = x
    1.18 -  | head A_ [] = null A_;
    1.19 -
    1.20 -val null_option : 'a option = NONE;
    1.21 -
    1.22 -fun null_optiona () = {null = null_option} : ('a option) null;
    1.23 -
    1.24 -val dummy : Nat.nat option =
    1.25 -  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    1.26 -
    1.27 -end; (*struct Codegen*)