isabelle-cookbook: CookBook/Package/Ind_Code.thy@64fa844064fa (annotated)

91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Ind_Code
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Base" Simple_Inductive_Package
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	text {*
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
118 5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	7	@{ML_chunk [display,gray] definitions_aux}
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	8	@{ML_chunk [display,gray,linenos] definitions}
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	9
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	10	*}
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	11
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	12	text {*
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	13
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	@{ML_chunk [display,gray] induction_rules}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	*}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	text {*
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	@{ML_chunk [display,gray] intro_rules}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
124 0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	22
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	*}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
124 0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	25	text {*
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	26	Things to include at the end:
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	27
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	28	\begin{itemize}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	29	\item say something about add-inductive-i to return
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	30	the rules
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	31	\item say that the induction principle is weaker (weaker than
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	32	what the standard inductive package generates)
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	33	\end{itemize}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	34
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	35	*}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	36
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	37
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 04 Mar 2009 14:26:21 +0000 (2009-03-04)
changeset 159	64fa844064fa
parent 124	0b9fa606a746
child 163	2319cff107f0
permissions	-rw-r--r--