isabelle-cookbook: ProgTutorial/ROOT.ML@386375b7a22a (annotated)

328 c0cae24b9d46 updated to new Isabelle; more work on the data section Christian Urban <urbanc@in.tum.de> parents: 327 diff changeset	1	quick_and_dirty := true;
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	2
27 104af757fbf0 Added chapter about writing packages. berghofe parents: 15 diff changeset	3	no_document use_thy "Base";
122 79696161ae16 polished Christian Urban <urbanc@in.tum.de> parents: 120 diff changeset	4	no_document use_thy "Package/Simple_Inductive_Package";
427 94538ddcac9b added example from Tobias and changed the title Christian Urban <urbanc@in.tum.de> parents: 395 diff changeset	5	no_document use_thy "~~/src/HOL/Number_Theory/Primes";
459 4532577b61e0 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 441 diff changeset	6	no_document use_thy "~~/src/HOL/Library/Efficient_Nat";
27 104af757fbf0 Added chapter about writing packages. berghofe parents: 15 diff changeset	7
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	8	use_thy "Intro";
441 520127b708e6 test Christian Urban <urbanc@in.tum.de> parents: 427 diff changeset	9	use_thy "First_Steps";
395 2c392f61f400 spilt the Essential's chapter Christian Urban <urbanc@in.tum.de> parents: 348 diff changeset	10	use_thy "Essential";
2c392f61f400 spilt the Essential's chapter Christian Urban <urbanc@in.tum.de> parents: 348 diff changeset	11	use_thy "Advanced";
329 5dffcab68680 more work Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	12
5dffcab68680 more work Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	13	no_document use_thy "Helper/Command/Command";
4 2a69b119cdee added verbatim the notes by Jeremy Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	14	use_thy "Parsing";
75 f2dea0465bb4 tuned Christian Urban <urbanc@in.tum.de> parents: 68 diff changeset	15	use_thy "Tactical";
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: 12 diff changeset	16
27 104af757fbf0 Added chapter about writing packages. berghofe parents: 15 diff changeset	17	use_thy "Package/Ind_Intro";
127 74846cb0fff9 updated and added two tentative recipes Christian Urban <urbanc@in.tum.de> parents: 122 diff changeset	18	use_thy "Package/Ind_Prelims";
74846cb0fff9 updated and added two tentative recipes Christian Urban <urbanc@in.tum.de> parents: 122 diff changeset	19	use_thy "Package/Ind_Interface";
27 104af757fbf0 Added chapter about writing packages. berghofe parents: 15 diff changeset	20	use_thy "Package/Ind_General_Scheme";
92 4e3f262a459d tuned Christian Urban <urbanc@in.tum.de> parents: 75 diff changeset	21	use_thy "Package/Ind_Code";
224 647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	22	use_thy "Package/Ind_Extensions";
27 104af757fbf0 Added chapter about writing packages. berghofe parents: 15 diff changeset	23
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: 12 diff changeset	24	use_thy "Appendix";
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 27 diff changeset	25	use_thy "Recipes/Antiquotes";
61 64c9540f2f84 Added four recipes. boehmes parents: 44 diff changeset	26	use_thy "Recipes/TimeLimit";
154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: 151 diff changeset	27	use_thy "Recipes/Timing";
427 94538ddcac9b added example from Tobias and changed the title Christian Urban <urbanc@in.tum.de> parents: 395 diff changeset	28	use_thy "Recipes/CallML";
61 64c9540f2f84 Added four recipes. boehmes parents: 44 diff changeset	29	use_thy "Recipes/ExternalSolver";
120 c39f83d8daeb some polishing; split up the file External Solver into two Christian Urban <urbanc@in.tum.de> parents: 92 diff changeset	30	use_thy "Recipes/Oracle";
127 74846cb0fff9 updated and added two tentative recipes Christian Urban <urbanc@in.tum.de> parents: 122 diff changeset	31	use_thy "Recipes/Sat";
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 127 diff changeset	32	use_thy "Recipes/USTypes";
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: 13 diff changeset	33
44 dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual Christian Urban <urbanc@in.tum.de> parents: 41 diff changeset	34	use_thy "Solutions";
348 2f2018927f2a tuned Christian Urban <urbanc@in.tum.de> parents: 329 diff changeset	35	(use_thy "Readme";)
68 e7519207c2b7 added more to the "new command section" and tuning Christian Urban <urbanc@in.tum.de> parents: 61 diff changeset	36

author	Christian Urban <urbanc@in.tum.de>
	Wed, 15 Feb 2012 14:47:46 +0000
changeset 511	386375b7a22a
parent 459	4532577b61e0
child 525	92a3600e50e4
permissions	-rw-r--r--