|
(** Test of the different syntaxes of SearchAbout, in particular
with and without the [ ... ] delimiters *)
SearchAbout plus.
SearchAbout plus mult.
SearchAbout "plus_n".
SearchAbout plus "plus_n".
SearchAbout "*".
SearchAbout "*" "+".
SearchAbout plus inside Peano.
SearchAbout plus mult inside Peano.
SearchAbout "plus_n" inside Peano.
SearchAbout plus "plus_n" inside Peano.
SearchAbout "*" inside Peano.
SearchAbout "*" "+" inside Peano.
SearchAbout plus outside Peano Logic.
SearchAbout plus mult outside Peano Logic.
SearchAbout "plus_n" outside Peano Logic.
SearchAbout plus "plus_n" outside Peano Logic.
SearchAbout "*" outside Peano Logic.
SearchAbout "*" "+" outside Peano Logic.
SearchAbout -"*" "+" outside Logic.
SearchAbout -"*"%nat "+"%nat outside Logic.
SearchAbout [plus].
SearchAbout [plus mult].
SearchAbout ["plus_n"].
SearchAbout [plus "plus_n"].
SearchAbout ["*"].
SearchAbout ["*" "+"].
SearchAbout [plus] inside Peano.
SearchAbout [plus mult] inside Peano.
SearchAbout ["plus_n"] inside Peano.
SearchAbout [plus "plus_n"] inside Peano.
SearchAbout ["*"] inside Peano.
SearchAbout ["*" "+"] inside Peano.
SearchAbout [plus] outside Peano Logic.
SearchAbout [plus mult] outside Peano Logic.
SearchAbout ["plus_n"] outside Peano Logic.
SearchAbout [plus "plus_n"] outside Peano Logic.
SearchAbout ["*"] outside Peano Logic.
SearchAbout ["*" "+"] outside Peano Logic.
SearchAbout [-"*" "+"] outside Logic.
SearchAbout [-"*"%nat "+"%nat] outside Logic.
(** The example in the Reference Manual *)
Require Import ZArith.
SearchAbout Z.mul Z.add "distr".
SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
