nominal2: Attic/Prove.thy@0b692f37a771 (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 =
319 0ae9d9e66cb7 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 183 diff changeset	12	Local_Theory.note (thm_name, (flat thms)) lthy \|> snd
48 5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	13
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	14	fun setup_proof (name_spec, (txt, pos)) lthy =
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	15	let
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	16	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	17	in
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 948 diff changeset	18	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	19	end
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
48 5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	21	val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	in
46 e801b929216b some tuning of my code Christian Urban <urbanc@in.tum.de> parents: 6 diff changeset	23	OuterSyntax.local_theory_to_proof "prove" "proving a proposition"
48 5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	24	OuterKeyword.thy_goal (parser >> setup_proof)
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	end
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
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 26 Apr 2010 08:08:20 +0200
changeset 1949	0b692f37a771
parent 948	25c4223635f4
child 2171	9697bbf713ec
permissions	-rw-r--r--