src/HOL/PreList.thy
changeset 10212 33fe2d701ddd
parent 9619 6125cc9efc18
child 10261 bb2f1e859177
equal deleted inserted replaced
10211:1bece7f35762 10212:33fe2d701ddd
     6 A basis for building theory List on. Is defined separately to serve as a
     6 A basis for building theory List on. Is defined separately to serve as a
     7 basis for theory ToyList in the documentation.
     7 basis for theory ToyList in the documentation.
     8 *)
     8 *)
     9 
     9 
    10 theory PreList =
    10 theory PreList =
    11   Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
    11   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    12   SVC_Oracle + While:
    12   Relation_Power + Calculation + SVC_Oracle + While:
    13 
    13 
    14 theorems [cases type: bool] = case_split
    14 theorems [cases type: bool] = case_split
    15 
    15 
    16 end
    16 end