2019-05-22 |
Norbert Schirmer |
polish document
|
file |
diff |
annotate
|
2019-05-21 |
Norbert Schirmer |
prefer more result checking in ML antiquotations
|
file |
diff |
annotate
|
2019-05-17 |
Norbert Schirmer |
prefer cartouches over " in ML antiquotations
|
file |
diff |
annotate
|
2019-05-16 |
Norbert Schirmer |
tuned ML-antiquotations; added intro portions.
|
file |
diff |
annotate
|
2019-05-14 |
Norbert Schirmer |
isabelle update_cartouches -t
|
file |
diff |
annotate
|
2019-05-14 |
Norbert Schirmer |
Accomodate to Isabelle 2018
|
file |
diff |
annotate
|
2013-04-19 |
Christian Urban |
updated to simplifier change
|
file |
diff |
annotate
|
2012-04-30 |
Christian Urban |
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
|
file |
diff |
annotate
|
2011-06-21 |
Christian Urban |
added an excercise originally by Jasmin Blanchette
|
file |
diff |
annotate
|
2011-02-23 |
Christian Urban |
updated to post-2011 Isabelle
|
file |
diff |
annotate
|
2010-08-13 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-08-13 |
Christian Urban |
added an example to be used for conversions later on
|
file |
diff |
annotate
|
2010-07-28 |
Christian Urban |
test
|
file |
diff |
annotate
|
2010-07-20 |
Christian Urban |
partially moved from string_of_term to pretty_term
|
file |
diff |
annotate
|
2010-05-27 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
2010-05-17 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-02 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-01 |
Christian Urban |
improved section on conversions
|
file |
diff |
annotate
|
2009-11-24 |
Christian Urban |
tuned solution with comb_conv
|
file |
diff |
annotate
|
2009-11-17 |
Christian Urban |
added exercise
|
file |
diff |
annotate
|
2009-10-19 |
Christian Urban |
polished theorem section
|
file |
diff |
annotate
|
2009-10-18 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
2009-10-13 |
Christian Urban |
tuned the ML-output mechanism; tuned slightly the text
|
file |
diff |
annotate
|
2009-10-03 |
Christian Urban |
more work
|
file |
diff |
annotate
|
2009-10-03 |
Christian Urban |
updated to new Isabelle; more work on the data section
|
file |
diff |
annotate
|
2009-08-20 |
Christian Urban |
further polishing of index generation
|
file |
diff |
annotate
|
2009-08-20 |
Christian Urban |
polished
|
file |
diff |
annotate
|
2009-08-19 |
Christian Urban |
polished the exercises about constructing terms
|
file |
diff |
annotate
|
2009-08-18 |
Christian Urban |
added exercise
|
file |
diff |
annotate
|
2009-07-28 |
Christian Urban |
slightly changed exercises about rev_sum
|
file |
diff |
annotate
|
2009-07-21 |
griff |
merged
|
file |
diff |
annotate
|
2009-07-21 |
griff |
modified solution(s) for "revsum" example
|
file |
diff |
annotate
|
2009-07-21 |
griff |
included an alternative solution for the "rev_sum" example as a comment
|
file |
diff |
annotate
|
2009-04-15 |
Christian Urban |
replaced "warning" with "writeln"
|
file |
diff |
annotate
|
2009-04-02 |
Christian Urban |
section for further material about simple inductive
|
file |
diff |
annotate
|
2009-03-30 |
Christian Urban |
updated to latest Isabelle
|
file |
diff |
annotate
|
2009-03-21 |
Christian Urban |
some polishing
|
file |
diff |
annotate
|
2009-03-19 |
Christian Urban |
made more of the transition from "CookBook" to "ProgTutorial"
|
file |
diff |
annotate
| base
|