equal
deleted
inserted
replaced
133 *) |
133 *) |
134 in |
134 in |
135 lthy |
135 lthy |
136 |> add_simps "simps" [] mutual_info fixes tsimps stmts |
136 |> add_simps "simps" [] mutual_info fixes tsimps stmts |
137 |> with_local_path defname |
137 |> with_local_path defname |
138 (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd) |
138 (LocalTheory.note (("induct", []), tinduct) #> snd) |
139 end |
139 end |
140 |
140 |
141 |
141 |
142 fun fundef_setup_termination_proof name_opt lthy = |
142 fun fundef_setup_termination_proof name_opt lthy = |
143 let |
143 let |