Quelle  join-module1.fake   Sprache: unbekannt

# Script simulating a dialog between rocqide and coqtop -ideslave
# Run it via fake_ide
#
# Join from within a module.
#

ADD { Lemma x : True. }
ADD { Proof. }
ADD { constructor. }
ADD { Qed. }
ADD { Module Foo. }
JOIN