summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 25 Nov 2011 12:18:39 +0100 | |

changeset 45638 | e5fd20f23241 |

parent 45629 | ef08425dd2d5 (current diff) |

parent 45637 | 5f85efcb50c1 (diff) |

child 45639 | efddd75c741e |

merged

--- a/src/HOL/IMP/Compiler.thy Fri Nov 25 10:52:30 2011 +0100 +++ b/src/HOL/IMP/Compiler.thy Fri Nov 25 12:18:39 2011 +0100 @@ -17,9 +17,8 @@ *} abbreviation "isize xs == int (length xs)" -primrec - inth :: "'a list => int => 'a" (infixl "!!" 100) where - inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))" +fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where +"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))" text {* The only additional lemma we need is indexing over append: @@ -41,7 +40,7 @@ JMPGE int type_synonym stack = "val list" -type_synonym config = "int\<times>state\<times>stack" +type_synonym config = "int \<times> state \<times> stack" abbreviation "hd2 xs == hd(tl xs)" abbreviation "tl2 xs == tl(tl xs)"