blob: ba64d959579bf4cbe412d547b66743cc13c3ed98 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* -*- isa -*-
Example theory file for Isabelle
David Aspinall <da@dcs.ed.ac.uk>
$Id$
The line at the top of this comment forces
Proof General's classic Isabelle mode;
scripting takes place in .ML files.
NB: this is incompatible with ProofGeneral/Isar which is
a separate instance of Proof General.
See the PG manual for ways to select Isabelle/Classic
by default.
*)
Example = Main
|