| changeset 514 | 7e25716c3744 |
| parent 442 | 7e33ba6190de |
| child 538 | e9fd5eff62c1 |
| 513:f223f8223d4a | 514:7e25716c3744 |
|---|---|
1 theory Simple_Inductive_Package |
1 theory Simple_Inductive_Package |
2 imports Main "../Base" |
2 imports Main "../Base" |
3 keywords "simple_inductive" :: thy_decl |
|
3 uses "simple_inductive_package.ML" |
4 uses "simple_inductive_package.ML" |
4 begin |
5 begin |
5 |
6 |
6 (* |
7 (* |
7 simple_inductive |
8 simple_inductive |