2009-10-30 Proof.goal
haftmann [Fri, 30 Oct 2009 09:42:17 +0100] rev 367
Proof.goal
2009-10-30 tuned
haftmann [Fri, 30 Oct 2009 09:42:17 +0100] rev 366
tuned
2009-10-30 avoid value restriction
haftmann [Fri, 30 Oct 2009 09:42:16 +0100] rev 365
avoid value restriction
2009-10-30 modernized
haftmann [Fri, 30 Oct 2009 09:42:16 +0100] rev 364
modernized
2009-10-29 tuned
Christian Urban <urbanc@in.tum.de> [Thu, 29 Oct 2009 19:09:27 +0100] rev 363
tuned
2009-10-29 added something about manual instantiations of theorems
Christian Urban <urbanc@in.tum.de> [Thu, 29 Oct 2009 16:02:15 +0100] rev 362
added something about manual instantiations of theorems
2009-10-27 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 15:43:21 +0100] rev 361
tuned
2009-10-25 tuned
Christian Urban <urbanc@in.tum.de> [Mon, 26 Oct 2009 00:00:26 +0100] rev 360
tuned
2009-10-25 polished
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 16:12:05 +0100] rev 359
polished
2009-10-25 some polishing
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 15:26:03 +0100] rev 358
some polishing
2009-10-22 included a comment from Tim Bourke
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 14:08:23 +0200] rev 357
included a comment from Tim Bourke
2009-10-22 updated to new Isabelle
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 02:03:14 +0200] rev 356
updated to new Isabelle
2009-10-20 added something about add_thms_dynamic
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 12:25:20 +0200] rev 355
added something about add_thms_dynamic
2009-10-19 some slight polishing
Christian Urban <urbanc@in.tum.de> [Mon, 19 Oct 2009 17:31:13 +0200] rev 354
some slight polishing
2009-10-19 completed section on theorems
Christian Urban <urbanc@in.tum.de> [Mon, 19 Oct 2009 14:10:42 +0200] rev 353
completed section on theorems
2009-10-19 polished theorem section
Christian Urban <urbanc@in.tum.de> [Mon, 19 Oct 2009 02:02:21 +0200] rev 352
polished theorem section
2009-10-18 updated to new Isabelle
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 21:22:44 +0200] rev 351
updated to new Isabelle
2009-10-18 polished
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 08:44:39 +0200] rev 350
polished
2009-10-14 updated to Isabelle changes
Christian Urban <urbanc@in.tum.de> [Wed, 14 Oct 2009 14:56:19 +0200] rev 349
updated to Isabelle changes
2009-10-14 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 14 Oct 2009 12:33:38 +0200] rev 348
tuned
2009-10-14 slightly tuned
Christian Urban <urbanc@in.tum.de> [Wed, 14 Oct 2009 02:32:53 +0200] rev 347
slightly tuned
2009-10-13 tuned the ML-output mechanism; tuned slightly the text
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 22:57:25 +0200] rev 346
tuned the ML-output mechanism; tuned slightly the text
2009-10-12 polished
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 17:07:17 +0200] rev 345
polished
2009-10-11 added structures in the index
Christian Urban <urbanc@in.tum.de> [Sun, 11 Oct 2009 23:16:34 +0200] rev 344
added structures in the index
2009-10-11 polished first chapter
Christian Urban <urbanc@in.tum.de> [Sun, 11 Oct 2009 22:45:29 +0200] rev 343
polished first chapter
2009-10-11 fixed glitch with tocibind
Christian Urban <urbanc@in.tum.de> [Sun, 11 Oct 2009 16:30:59 +0200] rev 342
fixed glitch with tocibind
2009-10-10 more work on theorem section
Christian Urban <urbanc@in.tum.de> [Sun, 11 Oct 2009 01:47:15 +0200] rev 341
more work on theorem section
2009-10-10 more work
Christian Urban <urbanc@in.tum.de> [Sat, 10 Oct 2009 20:27:51 +0200] rev 340
more work
2009-10-10 used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de> [Sat, 10 Oct 2009 18:25:43 +0200] rev 339
used a better implementation of \index in Latex; added more to the theorem section
2009-10-10 more on the theorem section
Christian Urban <urbanc@in.tum.de> [Sat, 10 Oct 2009 15:16:44 +0200] rev 338
more on the theorem section
2009-10-09 a bit more work on the theorem section
Christian Urban <urbanc@in.tum.de> [Fri, 09 Oct 2009 10:34:38 +0200] rev 337
a bit more work on the theorem section
2009-10-08 polished on the pretty printing section
Christian Urban <urbanc@in.tum.de> [Thu, 08 Oct 2009 21:49:11 +0200] rev 336
polished on the pretty printing section
2009-10-07 reorganised the certified terms section; tuned
Christian Urban <urbanc@in.tum.de> [Wed, 07 Oct 2009 11:28:40 +0200] rev 335
reorganised the certified terms section; tuned
2009-10-07 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 07 Oct 2009 09:54:01 +0200] rev 334
tuned
2009-10-06 added fixme
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 16:40:37 +0200] rev 333
added fixme
2009-10-06 added the function unabs_def in the conversions section
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:35:00 +0200] rev 332
added the function unabs_def in the conversions section
2009-10-05 used rewrite_goal_tac (instead of rewrite_goals_tac)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:45:49 +0200] rev 331
used rewrite_goal_tac (instead of rewrite_goals_tac)
2009-10-04 tuned
Christian Urban <urbanc@in.tum.de> [Sun, 04 Oct 2009 21:56:53 +0200] rev 330
tuned
2009-10-03 more work
Christian Urban <urbanc@in.tum.de> [Sat, 03 Oct 2009 19:10:23 +0200] rev 329
more work
2009-10-03 updated to new Isabelle; more work on the data section
Christian Urban <urbanc@in.tum.de> [Sat, 03 Oct 2009 13:01:39 +0200] rev 328
updated to new Isabelle; more work on the data section
2009-10-02 more work on the storing section
Christian Urban <urbanc@in.tum.de> [Fri, 02 Oct 2009 15:38:14 +0200] rev 327
more work on the storing section
2009-10-01 more work on the tutorial
Christian Urban <urbanc@in.tum.de> [Thu, 01 Oct 2009 10:19:21 +0200] rev 326
more work on the tutorial
2009-09-29 started section about storing data
Christian Urban <urbanc@in.tum.de> [Tue, 29 Sep 2009 22:10:48 +0200] rev 325
started section about storing data
2009-09-28 updated foobar_proof example
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 23:52:06 +0200] rev 324
updated foobar_proof example
2009-09-27 some polishing
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 01:21:27 +0200] rev 323
some polishing
2009-08-24 included some tests
Christian Urban <urbanc@in.tum.de> [Tue, 25 Aug 2009 00:07:37 +0200] rev 322
included some tests
2009-08-22 polished the commands section
Christian Urban <urbanc@in.tum.de> [Sat, 22 Aug 2009 02:56:08 +0200] rev 321
polished the commands section
2009-08-21 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 16:23:51 +0200] rev 320
tuned
2009-08-21 added file for producing a keyword file
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 16:04:59 +0200] rev 319
added file for producing a keyword file
2009-08-21 split up the first-steps section into two chapters
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 11:42:14 +0200] rev 318
split up the first-steps section into two chapters
2009-08-20 added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 23:30:51 +0200] rev 317
added an experimental antiquotation to replace eventually ML_response_fake
2009-08-20 further polishing of index generation
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 22:30:20 +0200] rev 316
further polishing of index generation
2009-08-20 simplified a bit the index generation
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 14:19:39 +0200] rev 315
simplified a bit the index generation
2009-08-20 polished
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 10:38:26 +0200] rev 314
polished
2009-08-19 polished the exercises about constructing terms
Christian Urban <urbanc@in.tum.de> [Wed, 19 Aug 2009 09:25:49 +0200] rev 313
polished the exercises about constructing terms
2009-08-18 added exercise
Christian Urban <urbanc@in.tum.de> [Wed, 19 Aug 2009 00:49:40 +0200] rev 312
added exercise
2009-08-17 polished
Christian Urban <urbanc@in.tum.de> [Tue, 18 Aug 2009 01:05:56 +0200] rev 311
polished
2009-08-17 added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de> [Mon, 17 Aug 2009 20:57:32 +0200] rev 310
added some rudimentary inrastructure for producing the ML-code
2009-08-16 tuned
Christian Urban <urbanc@in.tum.de> [Sun, 16 Aug 2009 22:14:36 +0200] rev 309
tuned
2009-08-16 improvements from the workshop
Christian Urban <urbanc@in.tum.de> [Sun, 16 Aug 2009 21:54:47 +0200] rev 308
improvements from the workshop
2009-08-13 suggestions by Peter Homeier
Christian Urban <urbanc@in.tum.de> [Thu, 13 Aug 2009 21:32:10 +0200] rev 307
suggestions by Peter Homeier
2009-08-05 tuned the section about printing several bits of inormation
Christian Urban <urbanc@in.tum.de> [Wed, 05 Aug 2009 16:00:01 +0200] rev 306
tuned the section about printing several bits of inormation
2009-08-05 added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de> [Wed, 05 Aug 2009 09:24:18 +0200] rev 305
added a comment for printing out information and tuned some examples accordingly
2009-08-05 polished comment for error function
Christian Urban <urbanc@in.tum.de> [Wed, 05 Aug 2009 08:58:28 +0200] rev 304
polished comment for error function
(0) -300 -100 -64 +64 +100 tip