Inductive definitions are now introduced earlier in the theory hierarchy.
datatype
'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
| Sum ('a aexp list)
| Diff ('a aexp) ('a aexp)
| Var 'a
| Num nat
and 'a bexp = Less ('a aexp) ('a aexp)
| And ('a bexp) ('a bexp)
| Neg ('a bexp)