equal
deleted
inserted
replaced
1572 then we can use this tactic to unfold the definition of this constant. |
1572 then we can use this tactic to unfold the definition of this constant. |
1573 *} |
1573 *} |
1574 |
1574 |
1575 lemma |
1575 lemma |
1576 shows "MyTrue \<Longrightarrow> True" |
1576 shows "MyTrue \<Longrightarrow> True" |
1577 apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *}) |
1577 apply(tactic {* rewrite_goal_tac @{context} @{thms MyTrue_def} 1 *}) |
1578 txt{* producing the goal state |
1578 txt{* producing the goal state |
1579 \begin{isabelle} |
1579 \begin{isabelle} |
1580 @{subgoals [display]} |
1580 @{subgoals [display]} |
1581 \end{isabelle} *} |
1581 \end{isabelle} *} |
1582 (*<*)oops(*>*) |
1582 (*<*)oops(*>*) |