| changeset 10212 | 33fe2d701ddd |
| parent 9619 | 6125cc9efc18 |
| child 10261 | bb2f1e859177 |
--- a/src/HOL/PreList.thy Thu Oct 12 18:09:06 2000 +0200 +++ b/src/HOL/PreList.thy Thu Oct 12 18:38:23 2000 +0200 @@ -8,8 +8,8 @@ *) theory PreList = - Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + - SVC_Oracle + While: + Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + + Relation_Power + Calculation + SVC_Oracle + While: theorems [cases type: bool] = case_split