nominal2: Attic/Prove.thy@fc4b3e367c86 (annotated)

6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Prove
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 319 diff changeset	2	imports Plain
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	ML {*
183 6acf9e001038 proved the two lemmas in QuotScript (reformulated them without leading forall) Christian Urban <urbanc@in.tum.de> parents: 83 diff changeset	6	val r = Unsynchronized.ref (NONE:(unit -> term) option)
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	*}
46 e801b929216b some tuning of my code Christian Urban <urbanc@in.tum.de> parents: 6 diff changeset	8
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	ML {*
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	let
48 5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	11	fun after_qed thm_name thms lthy =
2171 9697bbf713ec Isabelle renamings Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1949 diff changeset	12	Local_Theory.note (thm_name, (flat thms)) lthy \|> snd
9697bbf713ec Isabelle renamings Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1949 diff changeset	13	fun setup_proof (name_spec, (txt, _)) lthy =
48 5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	14	let
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	15	val trm = ML_Context.evaluate lthy true ("r", r) txt
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	16	in
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 948 diff changeset	17	Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
57 13be92f5b638 used new cong_tac Christian Urban <urbanc@in.tum.de> parents: 48 diff changeset	18	end
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
2171 9697bbf713ec Isabelle renamings Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1949 diff changeset	20	val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	in
2171 9697bbf713ec Isabelle renamings Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1949 diff changeset	22	Outer_Syntax.local_theory_to_proof "prove" "proving a proposition"
9697bbf713ec Isabelle renamings Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1949 diff changeset	23	Keyword.thy_goal (parser >> setup_proof)
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	end
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	*}
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 09 Nov 2011 11:44:01 +0000
changeset 3048	fc4b3e367c86
parent 2171	9697bbf713ec
permissions	-rw-r--r--