equal
deleted
inserted
replaced
11 scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof 
11 scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof 
12 documents\<close> instead (see also \chref{ch:proofs}). 
12 documents\<close> instead (see also \chref{ch:proofs}). 
13 
13 
14 Nonetheless, it is possible to emulate proof scripts by sequential 
14 Nonetheless, it is possible to emulate proof scripts by sequential 
15 refinements of a proof state in backwards mode, notably with the @{command 
15 refinements of a proof state in backwards mode, notably with the @{command 
16 apply} command (see \secref{sec:tacticcommands}). There are also various 
16 apply} command (see \secref{sec:tacticcommands}). 
17 proof methods that allow to refer to implicit goal state information that is 
17 
18 normally not accessible to structured Isar proofs (see 
18 There are also various proof methods that allow to refer to implicit goal 
19 \secref{sec:tactics}). 
19 state information that is not accessible to structured Isar proofs (see 

20 \secref{sec:tactics}). Note that the @{command subgoal} 

21 (\secref{sec:subgoal}) command usually eliminates the need for implicit goal 

22 state references. 
20 \<close> 
23 \<close> 
21 
24 
22 
25 
23 section \<open>Commands for stepwise refinement \label{sec:tacticcommands}\<close> 
26 section \<open>Commands for stepwise refinement \label{sec:tacticcommands}\<close> 
24 
27 
80 for experimentation and interactive exploration, and should be avoided in 
83 for experimentation and interactive exploration, and should be avoided in 
81 finished proofs. 
84 finished proofs. 
82 \<close> 
85 \<close> 
83 
86 
84 
87 
85 section \<open>Explicit subgoal structure\<close> 
88 section \<open>Explicit subgoal structure \label{sec:subgoal}\<close> 
86 
89 
87 text \<open> 
90 text \<open> 
88 \begin{matharray}{rcl} 
91 \begin{matharray}{rcl} 
89 @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\ 
92 @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\ 
90 \end{matharray} 
93 \end{matharray} 