equal
deleted
inserted
replaced
53 and "then" "from" "with" :: prf_chain % "proof" |
53 and "then" "from" "with" :: prf_chain % "proof" |
54 and "note" :: prf_decl % "proof" |
54 and "note" :: prf_decl % "proof" |
55 and "supply" :: prf_script % "proof" |
55 and "supply" :: prf_script % "proof" |
56 and "using" "unfolding" :: prf_decl % "proof" |
56 and "using" "unfolding" :: prf_decl % "proof" |
57 and "fix" "assume" "presume" "def" :: prf_asm % "proof" |
57 and "fix" "assume" "presume" "def" :: prf_asm % "proof" |
|
58 and "consider" :: prf_goal % "proof" |
58 and "obtain" :: prf_asm_goal % "proof" |
59 and "obtain" :: prf_asm_goal % "proof" |
59 and "guess" :: prf_asm_goal_script % "proof" |
60 and "guess" :: prf_asm_goal_script % "proof" |
60 and "let" "write" :: prf_decl % "proof" |
61 and "let" "write" :: prf_decl % "proof" |
61 and "case" :: prf_asm % "proof" |
62 and "case" :: prf_asm % "proof" |
62 and "{" :: prf_open % "proof" |
63 and "{" :: prf_open % "proof" |