etc/isar/ParsingBug1.thy


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