nominal2: Attic/Prove.thy@9eab1dfc14d2 (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
5d32a81cfe49 added name to prove Christian Urban <urbanc@in.tum.de> parents: 46 diff changeset	18	Proof.theorem_i 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>
	Thu, 22 Apr 2010 05:16:23 +0200 (2010-04-22)
changeset 1933	9eab1dfc14d2
parent 948	25c4223635f4
child 1949	0b692f37a771
permissions	-rw-r--r--