isabelle-cookbook: ProgTutorial/Base.thy@438703674711 (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"
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	4	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	5
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	6	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	7	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	8
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	9	ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
396 a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	10
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	11	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	12	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	13
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	14	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	15	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	16	(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	17
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	18	fun de_bruijn n =
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	19	HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close>
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	20
538 e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	21	ML_file "output_tutorial.ML"
e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	22	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	23
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	24	setup \<open>AntiquoteSetup.setup\<close>
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	25
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	26	end

author	Norbert Schirmer <norbert.schirmer@web.de>
	Tue, 21 May 2019 14:37:39 +0200
changeset 572	438703674711
parent 567	f7c97e64cc2a
child 573	321e220a6baa
permissions	-rw-r--r--