equal
deleted
inserted
replaced
|
1 (*$Id$ |
|
2 theory Main includes everything except AC*) |
1 |
3 |
2 (*$Id$ |
4 theory Main = Update + List + EquivClass + IntDiv + CardinalArith: |
3 theory Main includes everything*) |
|
4 |
|
5 theory Main = Update + InfDatatype + List + EquivClass + IntDiv: |
|
6 |
5 |
7 (* belongs to theory Trancl *) |
6 (* belongs to theory Trancl *) |
8 lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl] |
7 lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl] |
9 and trancl_induct = trancl_induct [case_names initial step, induct set: trancl] |
8 and trancl_induct = trancl_induct [case_names initial step, induct set: trancl] |
10 and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] |
9 and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] |