equal
deleted
inserted
replaced
76 |
76 |
77 |
77 |
78 exception REIF of string; |
78 exception REIF of string; |
79 |
79 |
80 fun dest_listT (Type (@{type_name "list"}, [T])) = T; |
80 fun dest_listT (Type (@{type_name "list"}, [T])) = T; |
81 |
|
82 (* This modified version of divide_and_conquer allows the threading |
|
83 of a state variable *) |
|
84 fun divide_and_conquer' decomp s x = |
|
85 let val ((ys, recomb), s') = decomp s x |
|
86 in recomb (fold_map (divide_and_conquer' decomp) ys s') end; |
|
87 |
81 |
88 fun rearrange congs = |
82 fun rearrange congs = |
89 let |
83 let |
90 fun P (_, th) = |
84 fun P (_, th) = |
91 let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th |
85 let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th |