blob: e56a5ae9b8c0c58e998e5a62a0cdf2170c5d4371 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(*
This is a small test case for parsing the { nested proof } phrase.
This case causes problems with the new parsing mechanism, see
comments in isar/isar-syntax.el and generic/proof-script.el
*)
theory ParsingBug1 imports Main begin
theorem "P"
proof -
assume a: "Q"
{fix i have "Q" sorry}
qed
|