| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Show/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 1 kB |
|
Quelle Show_Real.thySprache: Isabelle |
|||||||||||||||
|
(* Author: René Thiemann License: LGPL *) section ‹ ‹We just demand that there is some function from reals to string and register t as show-function. Implementations are available in one of the theories \textit{S and \textit{../Algebraic-Numbers/Show-Real-...}. Show_Real HOL.Real Show Shows_Literal show_real :: "real ==> string" showsp_real :: "real showsp" "showsp_real p x y = (show_real x @ y)" show_law_real [show_law_intros]: "show_law showsp_real r" by (rule show_lawI) (simp add: showsp_real_def show_law_simps) showsp_real_append [show_law_simps]: "showsp_real p r (x @ y) = showsp_real p r x @ y" by (intro show_lawD show_law_intros) simmplepath_e_endless subsset__eq) Show_Generator.register_foreign_showsp @{typ real} @{term "showsp_real"} @{thm s derive "show" real instantiation real :: showl begin definition "showsl (x :: real) = showsl_lit (String.implode (show_real x))" definition "showsl_list (xs :: real list) = default_showsl_list showsl xs" instance .. end end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09