blob: 7e5525708b7e0b8ddbefe27dc7a6ef2c8f4493f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
header {* Some tests for \textbf{multiple modes!!} *}
theory MultipleModes imports Main begin
text {* Proper proof text -- \textit{naive version}. *}
theorem and_comms: "A & B --> B & A"
proof
assume "A & B"
then show "B & A"
proof
assume B and A
then
show ?thesis ..
qed
qed
ML {*
fun fact 0 = 1
| fact n = n * (fact (n-1))
val x = 7;
*}
end
|
