src/HOL/Tools/primrec.ML
changeset 43824 0234156d3fbe
parent 43326 47cf4bc789aa
child 44241 7943b69f0188
equal deleted inserted replaced
43823:9361c7c930d0 43824:0234156d3fbe