equal
deleted
inserted
replaced
16 => ('a*('a uterm)) list" (infixl 56) |
16 => ('a*('a uterm)) list" (infixl 56) |
17 sdom :: "('a*('a uterm)) list => 'a set" |
17 sdom :: "('a*('a uterm)) list => 'a set" |
18 srange :: "('a*('a uterm)) list => 'a set" |
18 srange :: "('a*('a uterm)) list => 'a set" |
19 |
19 |
20 |
20 |
21 primrec "op <|" uterm |
21 primrec |
22 subst_Var "(Var v <| s) = assoc v (Var v) s" |
22 subst_Var "(Var v <| s) = assoc v (Var v) s" |
23 subst_Const "(Const c <| s) = Const c" |
23 subst_Const "(Const c <| s) = Const c" |
24 subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)" |
24 subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)" |
25 |
25 |
26 |
26 |