| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle appendix.thy Sprache: Isabelle |
|||||||||
|
(*<*)theory appendix
imports Main begin(*>*) text\<open> \begin{table}[htbp] \begin{center} \begin{tabular}{lll} Constant & Type & Syntax \\ \hline @{term [source] 0} & @{typeof [show_sorts] "0"} \\ @{term [source] 1} & @{typeof [show_sorts] "1"} \\ @{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\ @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\ @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\ @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\ @{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (inf @{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\ @{term [source] modulo} & @{typeof [show_sorts] "modulo"} & (infixl $mod$ 70) \\ @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\ @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\ @{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\ @{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\ @{term [source] top} & @{typeof [show_sorts] "top"} \\ @{term [source] bot} & @{typeof [show_sorts] "bot"} \end{tabular} \caption{Important Overloaded Constants in Main} \label{tab:overloading} \end{center} \end{table} \<close> (*<*)end(*>*) ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28