isabelle-cookbook: ProgTutorial/Base.thy@c3dbc04471a9 (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
573 321e220a6baa accomodate to upcoming Isabelle 2019 Norbert Schirmer <norbert.schirmer@web.de> parents: 572 diff changeset	6
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	7	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	8	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	9
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	10	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	11
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	12	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	13	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	14
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	15	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	16	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	17	(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	18
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	19	fun de_bruijn n =
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	20	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	21
538 e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	22	ML_file "output_tutorial.ML"
e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	23	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	24
565 cecd7a941885 isabelle update_cartouches -t Norbert Schirmer <norbert.schirmer@web.de> parents: 564 diff changeset	25	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	26
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	27	end

author	Norbert Schirmer <norbert.schirmer@web.de>
	Wed, 22 May 2019 13:24:30 +0200
changeset 575	c3dbc04471a9
parent 573	321e220a6baa
permissions	-rw-r--r--