equal
deleted
inserted
replaced
186 | ts_in (Inc ((_, ts), _)) = ts |
186 | ts_in (Inc ((_, ts), _)) = ts |
187 | ts_in (Sup (_, ts)) = ts |
187 | ts_in (Sup (_, ts)) = ts |
188 | ts_in (Mis _) = [] |
188 | ts_in (Mis _) = [] |
189 | ts_in _ = raise ERROR "ts_in: uncovered case in fun.def."; |
189 | ts_in _ = raise ERROR "ts_in: uncovered case in fun.def."; |
190 |
190 |
191 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM"; |
191 val unique = TermC.parseNEW'' @{theory "Real"} "UnIqE_tErM"; |
192 fun d_in (Cor ((d ,_), _)) = d |
192 fun d_in (Cor ((d ,_), _)) = d |
193 | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique) |
193 | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique) |
194 | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique) |
194 | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique) |
195 | d_in (Inc ((d, _), _)) = d |
195 | d_in (Inc ((d, _), _)) = d |
196 | d_in (Sup (d, _)) = d |
196 | d_in (Sup (d, _)) = d |