| changeset 12020 | a24373086908 |
| parent 11955 | 5818c5abb415 |
| child 12304 | 8df202daf55d |
--- a/src/HOL/PreList.thy Fri Nov 02 22:01:07 2001 +0100 +++ b/src/HOL/PreList.thy Fri Nov 02 22:01:58 2001 +0100 @@ -9,7 +9,10 @@ theory PreList = Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + - Relation_Power + Calculation + SVC_Oracle: + Relation_Power + SVC_Oracle: + +(*belongs to theory Divides*) +declare dvd_trans [trans] (*belongs to theory Wellfounded_Recursion*) declare wf_induct [induct set: wf]