isabelle-cookbook: ProgTutorial/Base.thy@6e2479089226 (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
564 6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	6	print_ML_antiquotations
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	7
564 6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	8	text \<open>Hallo ML Antiquotation:
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	9	@{ML \<open>2 + 3\<close>}
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	10	\<close>
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	11
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	12	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	13	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	14
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	15	ML %linenosgrayML{*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	16
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	17	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	18	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	19
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	20	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	21	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	22	(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	23
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	24	fun de_bruijn n =
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	25	HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
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
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	30
daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	31	(setup { OutputTutorial.setup }) (* Seems to be standard now, we don't need this anymoe *)
471 f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	32	setup {* AntiquoteSetup.setup *}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	33
564 6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	34	print_ML_antiquotations
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	35
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	36	text \<open>Hallo ML Antiquotation:
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	37	@{ML \<open>2 + 3\<close> }
6e2479089226 tuned parsing in document antiquotations for ML Norbert Schirmer <norbert.schirmer@web.de> parents: 562 diff changeset	38	\<close>
562 daf404920ab9 Accomodate to Isabelle 2018 Norbert Schirmer <norbert.schirmer@web.de> parents: 557 diff changeset	39
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	40	end

author	Norbert Schirmer <norbert.schirmer@web.de>
	Tue, 14 May 2019 16:59:53 +0200
changeset 564	6e2479089226
parent 562	daf404920ab9
child 565	cecd7a941885
permissions	-rw-r--r--