summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Tools/record.ML

changeset 32765 | 3032c0308019 |

parent 32764 | 690f9cccf232 |

child 32767 | 2885e2a09f72 |

equal
deleted
inserted
replaced

32764:690f9cccf232 | 32765:3032c0308019 |
---|---|

1730 val len = length fields; |
1730 val len = length fields; |

1731 val idxms = 0 upto len; |
1731 val idxms = 0 upto len; |

1732 |
1732 |

1733 (*before doing anything else, create the tree of new types |
1733 (*before doing anything else, create the tree of new types |

1734 that will back the record extension*) |
1734 that will back the record extension*) |

1735 (* FIXME cf. BalancedTree.make *) |
1735 (* FIXME cf. Balanced_Tree.make *) |

1736 fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], []) |
1736 fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], []) |

1737 | mktreeT [T] = T |
1737 | mktreeT [T] = T |

1738 | mktreeT xs = |
1738 | mktreeT xs = |

1739 let |
1739 let |

1740 val len = length xs; |
1740 val len = length xs; |

1743 val right = List.drop (xs, half); |
1743 val right = List.drop (xs, half); |

1744 in |
1744 in |

1745 HOLogic.mk_prodT (mktreeT left, mktreeT right) |
1745 HOLogic.mk_prodT (mktreeT left, mktreeT right) |

1746 end; |
1746 end; |

1747 |
1747 |

1748 (* FIXME cf. BalancedTree.make *) |
1748 (* FIXME cf. Balanced_Tree.make *) |

1749 fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], []) |
1749 fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], []) |

1750 | mktreeV [T] = T |
1750 | mktreeV [T] = T |

1751 | mktreeV xs = |
1751 | mktreeV xs = |

1752 let |
1752 let |

1753 val len = length xs; |
1753 val len = length xs; |