2010-07-16 haftmann [Fri, 16 Jul 2010 15:28:23 +0200] rev 37846
corrected range chec
src/HOL/Library/Efficient_Nat.thy

2010-07-16 haftmann [Fri, 16 Jul 2010 15:28:22 +0200] rev 37845
first roughly working version of Imperative HOL for Scala
src/HOL/Imperative_HOL/Array.thy src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Imperative_HOL/Imperative_HOL_ex.thy src/HOL/Imperative_HOL/Ref.thy src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy

2010-07-16 haftmann [Fri, 16 Jul 2010 14:11:08 +0200] rev 37844
tuned
src/Tools/Code/code_target.ML

2010-07-16 haftmann [Fri, 16 Jul 2010 13:58:37 +0200] rev 37843
merged

2010-07-16 haftmann [Fri, 16 Jul 2010 13:58:29 +0200] rev 37842
a first sketch for Imperative HOL witht Scala
src/HOL/Imperative_HOL/Array.thy src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Imperative_HOL/Ref.thy

2010-07-16 haftmann [Fri, 16 Jul 2010 13:57:46 +0200] rev 37841
don't fail gracefully
src/Tools/Code/code_thingol.ML

2010-07-16 haftmann [Fri, 16 Jul 2010 13:57:29 +0200] rev 37840
restored long-broken syntax sanity checks
src/Tools/Code/code_target.ML

2010-07-16 haftmann [Fri, 16 Jul 2010 13:57:29 +0200] rev 37839
tuned interpunctation
src/Tools/Code/code_simp.ML

2010-07-16 haftmann [Fri, 16 Jul 2010 10:23:21 +0200] rev 37838
fragments of Scala
src/HOL/Imperative_HOL/Heap_Monad.thy

2010-07-15 haftmann [Thu, 15 Jul 2010 10:16:17 +0200] rev 37837
merged