summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 07 Nov 2010 16:39:03 +0100 | |

changeset 40399 | a3acca2bddc9 |

parent 40398 | cdda2847a91e |

child 40400 | db905e068a60 |

'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);

--- a/src/Pure/Isar/isar_syn.ML Sat Nov 06 20:59:59 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sun Nov 07 16:39:03 2010 +0100 @@ -502,7 +502,7 @@ Outer_Syntax.local_theory_to_proof "example_proof" "example proof body, without any result" Keyword.thy_schematic_goal (Scan.succeed - (Specification.schematic_theorem_cmd "" NONE (K I) + (Specification.theorem_cmd "" NONE (K I) Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward)); val _ =