equal
deleted
inserted
replaced
194 val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = |
194 val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = |
195 map (calc_syntax definitional funprod) eqs'; |
195 map (calc_syntax definitional funprod) eqs'; |
196 in thy'' |
196 in thy'' |
197 |> ContConsts.add_consts_i |
197 |> ContConsts.add_consts_i |
198 (maps fst ctt @ |
198 (maps fst ctt @ |
199 (if length eqs'>1 then [const_copy] else[])@ |
199 (if length eqs'>1 andalso not definitional |
|
200 then [const_copy] else []) @ |
200 [const_bisim]) |
201 [const_bisim]) |
201 |> Sign.add_trrules_i (maps snd ctt) |
202 |> Sign.add_trrules_i (maps snd ctt) |
202 end; (* let *) |
203 end; (* let *) |
203 |
204 |
204 end; (* struct *) |
205 end; (* struct *) |