equal
deleted
inserted
replaced
1 (* Title: Pure/Isar/rule_cases.ML |
1 (* Title: Pure/Isar/rule_cases.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Manage local contexts of rules. |
5 Manage local contexts of rules. |
6 |
|
7 TODO: |
|
8 - instantiation of cases (including type vars!); |
|
9 *) |
6 *) |
10 |
7 |
11 signature RULE_CASES = |
8 signature RULE_CASES = |
12 sig |
9 sig |
13 type T (* = (string * typ) list * term list *) |
10 type T (* = (string * typ) list * term list *) |