ProgTutorial/Solutions.thy
Wed, 22 May 2019 12:38:51 +0200 Norbert Schirmer polish document
Tue, 21 May 2019 14:37:39 +0200 Norbert Schirmer prefer more result checking in ML antiquotations
Fri, 17 May 2019 10:38:01 +0200 Norbert Schirmer prefer cartouches over " in ML antiquotations
Thu, 16 May 2019 19:56:12 +0200 Norbert Schirmer tuned ML-antiquotations; added intro portions.
Tue, 14 May 2019 17:10:47 +0200 Norbert Schirmer isabelle update_cartouches -t
Tue, 14 May 2019 11:10:53 +0200 Norbert Schirmer Accomodate to Isabelle 2018
Fri, 19 Apr 2013 11:09:18 +0100 Christian Urban updated to simplifier change
Mon, 30 Apr 2012 14:43:52 +0100 Christian Urban removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Tue, 21 Jun 2011 12:53:16 +0100 Christian Urban added an excercise originally by Jasmin Blanchette
Wed, 23 Feb 2011 23:55:37 +0000 Christian Urban updated to post-2011 Isabelle
Fri, 13 Aug 2010 18:52:16 +0800 Christian Urban tuned
Fri, 13 Aug 2010 18:42:58 +0800 Christian Urban added an example to be used for conversions later on
Wed, 28 Jul 2010 19:09:49 +0200 Christian Urban test
Tue, 20 Jul 2010 13:34:44 +0100 Christian Urban partially moved from string_of_term to pretty_term
Thu, 27 May 2010 10:39:07 +0200 Christian Urban updated to new Isabelle
Mon, 17 May 2010 18:20:48 +0100 Christian Urban updated to new Isabelle
Thu, 03 Dec 2009 14:19:13 +0100 Christian Urban tuned
Wed, 02 Dec 2009 03:46:32 +0100 Christian Urban tuned
Tue, 01 Dec 2009 12:25:34 +0100 Christian Urban improved section on conversions
Tue, 24 Nov 2009 16:34:39 +0100 Christian Urban tuned solution with comb_conv
Tue, 17 Nov 2009 20:36:18 +0100 Christian Urban added exercise
Mon, 19 Oct 2009 02:02:21 +0200 Christian Urban polished theorem section
Sun, 18 Oct 2009 21:22:44 +0200 Christian Urban updated to new Isabelle
Tue, 13 Oct 2009 22:57:25 +0200 Christian Urban tuned the ML-output mechanism; tuned slightly the text
Sat, 03 Oct 2009 19:10:23 +0200 Christian Urban more work
Sat, 03 Oct 2009 13:01:39 +0200 Christian Urban updated to new Isabelle; more work on the data section
Thu, 20 Aug 2009 22:30:20 +0200 Christian Urban further polishing of index generation
Thu, 20 Aug 2009 10:38:26 +0200 Christian Urban polished
Wed, 19 Aug 2009 09:25:49 +0200 Christian Urban polished the exercises about constructing terms
Wed, 19 Aug 2009 00:49:40 +0200 Christian Urban added exercise
Tue, 28 Jul 2009 12:11:33 +0200 Christian Urban slightly changed exercises about rev_sum
Tue, 21 Jul 2009 12:49:26 +0200 griff merged
Tue, 21 Jul 2009 12:27:12 +0200 griff modified solution(s) for "revsum" example
Tue, 21 Jul 2009 12:11:24 +0200 griff included an alternative solution for the "rev_sum" example as a comment
Wed, 15 Apr 2009 13:11:08 +0000 Christian Urban replaced "warning" with "writeln"
Thu, 02 Apr 2009 11:48:35 +0100 Christian Urban section for further material about simple inductive
Mon, 30 Mar 2009 09:33:50 +0100 Christian Urban updated to latest Isabelle
Sat, 21 Mar 2009 12:35:03 +0100 Christian Urban some polishing
Thu, 19 Mar 2009 13:28:16 +0100 Christian Urban made more of the transition from "CookBook" to "ProgTutorial"
less more (0) tip