Tactic Notation "foo" hyp_list(hs) := clear hs.
Tactic Notation "bar" hyp_list(hs) := foo hs.
Goal True.
do 5 pose proof 0 as ?n0.
foo n1 n2.
bar n3 n4.
Abort.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.14Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|