This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
syntax [2011/05/07 12:21] 178.26.109.100 created |
syntax [2011/05/07 12:24] (current) 178.26.109.100 |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ===== Reserved Words ===== | + | ====== Isabelle/HOL Syntax ====== |
| This is one of the most important sections of the Wiki. Here you'll find the basic reserved words used in Isabelle/HOL, how should they be called, in which context, their meaning and hopefully some example code. If you're uploading/updating content, please try to adapt to the schema used for all the words to improve readability. | This is one of the most important sections of the Wiki. Here you'll find the basic reserved words used in Isabelle/HOL, how should they be called, in which context, their meaning and hopefully some example code. If you're uploading/updating content, please try to adapt to the schema used for all the words to improve readability. | ||
| - | === theory === | + | ===== Keywords ===== |
| + | |||
| + | ==== theory ==== | ||
| theory //name// | theory //name// | ||
| Line 101: | Line 103: | ||
| value "myMap ((op +)1) ((1::nat) # 3 # [])" | value "myMap ((op +)1) ((1::nat) # 3 # [])" | ||
| </code> | </code> | ||
| + | |||
| + | ===== Symbols from Libraries ===== | ||
| ==== Cons ==== | ==== Cons ==== | ||
| Line 117: | Line 121: | ||
| value "0 # 1 # 2 # 3 # []" | value "0 # 1 # 2 # 3 # []" | ||
| </code> | </code> | ||
| + | |||
| + | ===== Template ===== | ||
| ==== TERM ==== | ==== TERM ==== | ||