Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Tools/fixrec.ML
changeset 45897 65cef0298158
parent 45787 9fcaf2557c59
child 46895 de5cfda8b2de
equal deleted inserted replaced
45896:100fb1f33e3e 45897:65cef0298158 
   324 (*************************************************************************)
 
   324 (*************************************************************************)
 
   325 (************************* Main fixrec function **************************)
 
   325 (************************* Main fixrec function **************************)
 
   326 (*************************************************************************)
 
   326 (*************************************************************************)
 
   327 
   327 
   328 local
 
   328 local
 
   329 (* code adapted from HOL/Tools/primrec.ML *)
 
   329 (* code adapted from HOL/Tools/Datatype/primrec.ML *)
 
   330 
   330 
   331 fun gen_fixrec
 
   331 fun gen_fixrec
 
   332   prep_spec
 
   332   prep_spec
 
   333   (raw_fixes : (binding * 'a option * mixfix) list)
 
   333   (raw_fixes : (binding * 'a option * mixfix) list)
 
   334   (raw_spec' : (bool * (Attrib.binding * 'b)) list)
 
   334   (raw_spec' : (bool * (Attrib.binding * 'b)) list)
isabelle