equal
deleted
inserted
replaced
42 syntax (latex output) |
42 syntax (latex output) |
43 length :: "'a list \<Rightarrow> nat" ("|_|") |
43 length :: "'a list \<Rightarrow> nat" ("|_|") |
44 |
44 |
45 (* nth *) |
45 (* nth *) |
46 syntax (latex output) |
46 syntax (latex output) |
47 nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:$_{[\mathit{>_\<^raw:}]}$>" [1000,0] 1000) |
47 nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000) |
48 |
48 |
49 (* DUMMY *) |
49 (* DUMMY *) |
50 consts DUMMY :: 'a ("\<^raw:\_>") |
50 consts DUMMY :: 'a ("\<^raw:\_>") |
51 |
51 |
52 (* THEOREMS *) |
52 (* THEOREMS *) |