author | wenzelm |

Sat Dec 19 15:20:38 2015 +0100 (2015-12-19) | |

changeset 61866 | 6fa60a4f7e48 |

parent 61865 | 6dcc9e4f1aa6 |

child 61867 | 95cce5313c83 |

tuned;

1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 15:14:59 2015 +0100 1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 15:20:38 2015 +0100 1.3 @@ -102,8 +102,8 @@ 1.4 apply} sequences. 1.5 1.6 The current goal state, which is essentially a hidden part of the Isar/VM 1.7 - configurtation, is turned into a proof context and remaining conclusion. 1.8 - This correponds to @{command fix}~/ @{command assume}~/ @{command show} in 1.9 + configuration, is turned into a proof context and remaining conclusion. 1.10 + This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in 1.11 structured proofs, but the text of the parameters, premises and conclusion 1.12 is not given explicitly. 1.13