doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
author haftmann
Fri, 26 Jan 2007 09:24:35 +0100
changeset 22188 a63889770d57
parent 22015 12b94d7f7e1f
child 22386 4ebe883b02ff
permissions -rw-r--r--
adjusted manual to improved treatment of overloaded constants
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21190
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     1
structure ROOT = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     2
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     3
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     4
structure Nat = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     5
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     6
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     7
datatype nat = Zero_nat | Suc of nat;
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     8
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     9
end; (*struct Nat*)
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    10
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    11
structure Codegen = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    12
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    13
22015
12b94d7f7e1f adaptions
haftmann
parents: 21993
diff changeset
    14
val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
21190
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    15
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    16
val foobar_set : Nat.nat list =
22015
12b94d7f7e1f adaptions
haftmann
parents: 21993
diff changeset
    17
  Nat.Zero_nat ::
12b94d7f7e1f adaptions
haftmann
parents: 21993
diff changeset
    18
    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
21190
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    19
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    20
end; (*struct Codegen*)
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    21
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    22
end; (*struct ROOT*)