User Tools
references
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
references [2011/05/07 12:14] 178.26.109.100 created |
references [2011/05/28 17:26] (current) 131.246.229.97 |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ===== External References ===== | + | ====== External References ====== |
| Put here some links to other documentation sources that can be useful. | Put here some links to other documentation sources that can be useful. | ||
| + | |||
| + | * [[http://www.cl.cam.ac.uk/research/hvg/isabelle/faq.html|Isabelle FAQ]] | ||
| + | * [[http://isabelle.in.tum.de/dist/Isabelle/doc/main.pdf|What's is Main]] (by Tobias Nipkow) contains a list of populer datatypes and functions (i.e. there signatures) in the Main theory. | ||
| + | * [[http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf|A Proof Assistant for Higher-Order Logic]] (by Nipkow et al.) is an extensive tutorial to most of Isabelle's features. Find explanations for most methods, tactics, ... via the index. | ||
| + | |||
| * For a list of pre-defined symbols in Isabelle/HOL see Appendix B of [[http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/isar-ref.pdf|this document.]] Useful when the set of UNICODE characters is not available. | * For a list of pre-defined symbols in Isabelle/HOL see Appendix B of [[http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/isar-ref.pdf|this document.]] Useful when the set of UNICODE characters is not available. | ||
| * Presentation of Sheet 2 can be found [[https://docs.google.com/present/view?id=dhqv6v76_94dghtz9ct&interval=60|here]]. | * Presentation of Sheet 2 can be found [[https://docs.google.com/present/view?id=dhqv6v76_94dghtz9ct&interval=60|here]]. | ||
| + | * Presentation of Sheet 4 can be found [[https://docs.google.com/viewer?a=v&pid=explorer&chrome=true&srcid=0B8eH3X88xuy4N2NiMzY0ODktZjg1MS00YzEyLWExYzgtYmZjNjM3YmYyNmY3&hl=de&authkey=CJjn1YoM|here]] | ||
| + | * [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.5.3152&rep=rep1&type=pdf|"Executing Higher Order Logics"]] is a paper making an overview of how to write functions on Isabelle/HOL and some performance issues. Good about it is that it has some code and goes over some concepts that we've seen in the lectures/tutorials | ||
| + | * [[http://www.cs.uu.nl/research/techreps/repo/CS-2000/2000-09.pdf|Defining a non-concrete recursive type in HOL which includes sets]] is a report that at the beginning has some complementary information about type definition in HOL. Then it's just a bunch of theorems I didn't went through. | ||
references.1304763254.txt.gz · Last modified: 2011/05/07 12:14 by 178.26.109.100
Page Tools
