equal
deleted
inserted
replaced
172 val cont_thm = |
172 val cont_thm = |
173 Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) |
173 Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) |
174 (K (beta_tac 1)); |
174 (K (beta_tac 1)); |
175 val tuple_unfold_thm = |
175 val tuple_unfold_thm = |
176 (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
176 (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
177 |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv}; |
177 |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv}; |
178 |
178 |
179 fun mk_unfold_thms [] thm = [] |
179 fun mk_unfold_thms [] thm = [] |
180 | mk_unfold_thms (n::[]) thm = [(n, thm)] |
180 | mk_unfold_thms (n::[]) thm = [(n, thm)] |
181 | mk_unfold_thms (n::ns) thm = let |
181 | mk_unfold_thms (n::ns) thm = let |
182 val thmL = thm RS @{thm Pair_eqD1}; |
182 val thmL = thm RS @{thm Pair_eqD1}; |