isabelle-cookbook: ProgTutorial/Base.thy@e9fd5eff62c1 (annotated)

23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	1	theory Base
459 4532577b61e0 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 441 diff changeset	2	imports Main
4532577b61e0 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 441 diff changeset	3	"~~/src/HOL/Library/LaTeXsugar"
535 5734ab5dd86d adapted to new build framework Christian Urban <urbanc@in.tum.de> parents: 517 diff changeset	4	(*keywords "ML" "setup" "local_setup" :: thy_decl and
514 7e25716c3744 updated to outer syntax / parser changes Christian Urban <urbanc@in.tum.de> parents: 488 diff changeset	5	"ML_prf" :: prf_decl and
7e25716c3744 updated to outer syntax / parser changes Christian Urban <urbanc@in.tum.de> parents: 488 diff changeset	6	"ML_val" :: diag
535 5734ab5dd86d adapted to new build framework Christian Urban <urbanc@in.tum.de> parents: 517 diff changeset	7	*)
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	8	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	9
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	10	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	11	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	12
396 a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	13	ML {*
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	14	fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	15
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	16	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	17	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	18
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	19	fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	20	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	21	(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	22
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	23	fun de_bruijn n =
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	24	HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	25	*}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	26
538 e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	27	ML_file "output_tutorial.ML"
e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	28	ML_file "antiquote_setup.ML"
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	29
471 f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	30	setup {* OutputTutorial.setup *}
f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	31	setup {* AntiquoteSetup.setup *}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	32
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	33	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 04 Oct 2012 13:00:31 +0100
changeset 538	e9fd5eff62c1
parent 535	5734ab5dd86d
child 557	77ea2de0ca62
permissions	-rw-r--r--