blob: e1a783abefb8415258901b39d5256f2c5862d4fe (
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 = Main:
theorem "P"
proof -
assume a: "Q"
{fix i have "Q" sorry}
qed
|