Columbo aufrufen.mlg zum Wurzelverzeichnis wechselnShell {Shell[45] Isabelle[83] Cobol[109]}Datei anzeigen
DECLARE PLUGIN "tuto0_plugin"
{
open Pp
open Ltac_plugin
}
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
END
TACTIC EXTEND hello_world_tactic
| [ "hello_world" ] ->
{ let _ = Feedback.msg_notice (str Tuto0_main.message) in
Tacticals.New.tclIDTAC }
END
[ Original von:0.60Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
]
