src/HOLCF/Fixrec.thy
changeset 16758 c32334d98fcd
parent 16754 1b979f8b7e8e
child 16776 a3899ac14a1c
equal deleted inserted replaced
16757:b8bfd086f7d4 16758:c32334d98fcd
   213 val cpair_eqD1 = thm "cpair_eqD1";
   213 val cpair_eqD1 = thm "cpair_eqD1";
   214 val cpair_eqD2 = thm "cpair_eqD2";
   214 val cpair_eqD2 = thm "cpair_eqD2";
   215 val ssubst_lhs = thm "ssubst_lhs";
   215 val ssubst_lhs = thm "ssubst_lhs";
   216 *}
   216 *}
   217 
   217 
   218 subsection {* Intitializing the fixrec package *}
   218 subsection {* Initializing the fixrec package *}
   219 
   219 
   220 use "fixrec_package.ML"
   220 use "fixrec_package.ML"
   221 
   221 
   222 end
   222 end