|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Hyperreal.thy
Sprache: Isabelle
|
|
section \<open>Concrete Syntax\<close>
theory Quote_Antiquote imports Main begin
syntax
"_quote" :: "'b \ ('a \ 'b)" ("(\_\)" [0] 1000)
"_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000)
"_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000)
translations
"\b\" \ "CONST Collect \b\"
parse_translation \<open>
let
fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\<open>_antiquote\<close> t
| quote_tr ts = raise TERM ("quote_tr", ts);
in [(\<^syntax_const>\<open>_quote\<close>, K quote_tr)] end
\<close>
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
