src/HOL/PreList.thy
changeset 10261 bb2f1e859177
parent 10212 33fe2d701ddd
child 10519 ade64af4c57c
equal deleted inserted replaced
10260:6c31c8bb78e8 10261:bb2f1e859177
     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 + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    11   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    12   Relation_Power + Calculation + SVC_Oracle + While:
    12   Relation_Power + Calculation + SVC_Oracle:
    13 
    13 
    14 theorems [cases type: bool] = case_split
    14 (*belongs to theory HOL*)
       
    15 declare case_split [cases type: bool]
       
    16 
       
    17 (*belongs to theory Wellfounded_Recursion*)
       
    18 declare wf_induct [induct set: wf]
    15 
    19 
    16 end
    20 end