equal
deleted
inserted
replaced
30 lemma "ok1 \<and> ok2 \<and> doubtful" |
30 lemma "ok1 \<and> ok2 \<and> doubtful" |
31 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
31 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
32 prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *} |
32 prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *} |
33 oops |
33 oops |
34 |
34 |
35 lemma "thing1 \<and> thing2 \<and> thing3 \<and> thing4 \<and> thing5 \<and> thing6" |
35 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6" |
36 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
36 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
37 pr 2 |
37 pr 2 |
38 txt{* @{subgoals[display,indent=0,margin=65]} *} |
38 txt{* @{subgoals[display,indent=0,margin=65]} |
|
39 A total of 6 subgoals... |
|
40 *} |
39 oops |
41 oops |
40 |
42 |
41 |
43 |
42 |
44 |
43 (*needed??*) |
45 (*needed??*) |