| Tue, 21 May 2019 14:37:39 +0200 |
Norbert Schirmer |
prefer more result checking in ML antiquotations
|
file |
diff |
annotate
|
| Fri, 17 May 2019 10:38:01 +0200 |
Norbert Schirmer |
prefer cartouches over " in ML antiquotations
|
file |
diff |
annotate
|
| Thu, 16 May 2019 19:56:12 +0200 |
Norbert Schirmer |
tuned ML-antiquotations; added intro portions.
|
file |
diff |
annotate
|
| Tue, 14 May 2019 17:10:47 +0200 |
Norbert Schirmer |
isabelle update_cartouches -t
|
file |
diff |
annotate
|
| Tue, 14 May 2019 11:10:53 +0200 |
Norbert Schirmer |
Accomodate to Isabelle 2018
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 23:49:05 +0000 |
Christian Urban |
updated to latest isabelle
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 14:43:52 +0100 |
Christian Urban |
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
|
file |
diff |
annotate
|
| Wed, 26 Oct 2011 12:59:44 +0100 |
Christian Urban |
updated to post-2011-1 Isabelle
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 22:56:52 +0800 |
Christian Urban |
added something about Goal.prove_multi
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 19:09:49 +0200 |
Christian Urban |
test
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 13:34:44 +0100 |
Christian Urban |
partially moved from string_of_term to pretty_term
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 21:15:05 +0100 |
Christian Urban |
updated to new isabelle
|
file |
diff |
annotate
|
| Sun, 22 Nov 2009 15:27:10 +0100 |
Christian Urban |
updated to new Isabelle and clarified Skip_Proof
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 14:11:50 +0100 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
| Sat, 07 Nov 2009 01:03:37 +0100 |
Christian Urban |
added type work and updated to Isabelle and poly 5.3
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 10:49:25 +0100 |
Christian Urban |
tuned index
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 15:26:03 +0100 |
Christian Urban |
some polishing
|
file |
diff |
annotate
|
| Tue, 13 Oct 2009 22:57:25 +0200 |
Christian Urban |
tuned the ML-output mechanism; tuned slightly the text
|
file |
diff |
annotate
|
| Sun, 11 Oct 2009 16:30:59 +0200 |
Christian Urban |
fixed glitch with tocibind
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 11:45:49 +0200 |
Christian Urban |
used rewrite_goal_tac (instead of rewrite_goals_tac)
|
file |
diff |
annotate
|
| Sat, 03 Oct 2009 19:10:23 +0200 |
Christian Urban |
more work
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 01:21:27 +0200 |
Christian Urban |
some polishing
|
file |
diff |
annotate
|
| Thu, 20 Aug 2009 22:30:20 +0200 |
Christian Urban |
further polishing of index generation
|
file |
diff |
annotate
|
| Thu, 20 Aug 2009 14:19:39 +0200 |
Christian Urban |
simplified a bit the index generation
|
file |
diff |
annotate
|
| Wed, 05 Aug 2009 09:24:18 +0200 |
Christian Urban |
added a comment for printing out information and tuned some examples accordingly
|
file |
diff |
annotate
|
| Mon, 03 Aug 2009 14:01:57 +0200 |
Christian Urban |
replaced "writeln" with "tracing"
|
file |
diff |
annotate
|
| Sun, 02 Aug 2009 08:44:41 +0200 |
Christian Urban |
updated to Isabelle changes and merged sections in the FirstSteps chapter
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 15:51:51 +0200 |
Christian Urban |
polished the package chapter used FOCUS to explain the subproofs
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 11:38:52 +0200 |
Christian Urban |
made changes for SUBPROOF and sat_tac
|
file |
diff |
annotate
|
| Sat, 30 May 2009 17:40:20 +0200 |
Christian Urban |
added some first index-information
|
file |
diff |
annotate
|
| Sun, 17 May 2009 16:22:27 +0200 |
Christian Urban |
some polishing; added together with Jasmin more examples to the pretty printing section
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 13:11:08 +0000 |
Christian Urban |
replaced "warning" with "writeln"
|
file |
diff |
annotate
|
| Sat, 11 Apr 2009 19:23:58 +0000 |
Christian Urban |
very slight polishing to the simple inductive chapter
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 15:42:47 +0100 |
Christian Urban |
finished the heavy duty stuff for the inductive package
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 12:26:56 +0100 |
Christian Urban |
more work on the simple inductive chapter
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 20:31:18 +0100 |
Christian Urban |
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 16:50:13 +0100 |
Christian Urban |
used antiquotations
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 15:48:53 +0100 |
Christian Urban |
more work on the inductive package
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 18:19:42 +0000 |
Christian Urban |
polishing
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 12:49:28 +0000 |
Christian Urban |
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 19:00:51 +0000 |
Christian Urban |
more work on the simple inductive section
|
file |
diff |
annotate
|
| Wed, 25 Mar 2009 15:09:04 +0100 |
Christian Urban |
soem slight polishing
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 18:06:20 +0100 |
Christian Urban |
a bit more work on the simple-inductive package
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 18:17:24 +0100 |
Christian Urban |
some polishing
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 12:35:03 +0100 |
Christian Urban |
some polishing
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 17:50:28 +0100 |
Christian Urban |
more one the simple-inductive chapter
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:16 +0100 |
Christian Urban |
made more of the transition from "CookBook" to "ProgTutorial"
|
file |
diff |
annotate
| base
|