isabelle-cookbook: CookBook/Package/Ind_Code.thy@2319cff107f0 (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 {*
163 2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive Christian Urban <urbanc@in.tum.de> parents: 124 diff changeset	6	What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive Christian Urban <urbanc@in.tum.de> parents: 124 diff changeset	7	*}
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive Christian Urban <urbanc@in.tum.de> parents: 124 diff changeset	8
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive Christian Urban <urbanc@in.tum.de> parents: 124 diff changeset	9
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive Christian Urban <urbanc@in.tum.de> parents: 124 diff changeset	10	text {*
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	11
118 5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	12	@{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	13	@{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	14
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	15	*}
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	16
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	17	text {*
5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 110 diff changeset	18
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	@{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	20
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	*}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	text {*
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	@{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	26
124 0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	27
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	*}
667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
124 0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	30	text {*
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	31	Things to include at the end:
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	32
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	33	\begin{itemize}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	34	\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	35	the rules
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	36	\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	37	what the standard inductive package generates)
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	38	\end{itemize}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	39
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	40	*}
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	41
0b9fa606a746 added to the first-steps section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	42
91 667a0943c40b added a section that will eventually describe the code Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	end

author	Christian Urban <urbanc@in.tum.de>
	Sun, 08 Mar 2009 20:53:00 +0000 (2009-03-08)
changeset 163	2319cff107f0
parent 124	0b9fa606a746
child 164	3f617d7a2691
permissions	-rw-r--r--