equal
deleted
inserted
replaced
11 (*Object-level rules*) |
11 (*Object-level rules*) |
12 datatype orule = Subgoal of cterm |
12 datatype orule = Subgoal of cterm |
13 | Asm of int |
13 | Asm of int |
14 | Res of deriv |
14 | Res of deriv |
15 | Equal of deriv |
15 | Equal of deriv |
16 | Thm of string |
16 | Thm of string * tag list |
17 | Other of deriv; |
17 | Other of deriv; |
18 |
18 |
19 val size : deriv -> int |
19 val size : deriv -> int |
20 val drop : 'a mtree * int -> 'a mtree |
20 val drop : 'a mtree * int -> 'a mtree |
21 val linear : deriv -> deriv list |
21 val linear : deriv -> deriv list |
47 (*Object-level rules*) |
47 (*Object-level rules*) |
48 datatype orule = Subgoal of cterm |
48 datatype orule = Subgoal of cterm |
49 | Asm of int |
49 | Asm of int |
50 | Res of deriv |
50 | Res of deriv |
51 | Equal of deriv |
51 | Equal of deriv |
52 | Thm of string |
52 | Thm of string * tag list |
53 | Other of deriv; |
53 | Other of deriv; |
54 |
54 |
55 (*At position i, splice in value x, removing ngoal elements*) |
55 (*At position i, splice in value x, removing ngoal elements*) |
56 fun splice (i,x,ngoal,prfs) = |
56 fun splice (i,x,ngoal,prfs) = |
57 let val prfs0 = take(i-1,prfs) |
57 let val prfs0 = take(i-1,prfs) |