ProgTutorial/Package/Simple_Inductive_Package.thy
changeset 442 7e33ba6190de
parent 316 74f0a06f751f
child 514 7e25716c3744
equal deleted inserted replaced
440:a0b280dd4bc7 442:7e33ba6190de
    52 
    52 
    53 thm rel.accpartI'
    53 thm rel.accpartI'
    54 thm rel.accpart'.induct
    54 thm rel.accpart'.induct
    55 *)
    55 *)
    56 
    56 
    57 use "simple_inductive_package.ML"
       
    58 
    57 
    59 
    58 
    60 end
    59 end