This is an old revision of the document!

====== Rich Model Language ====== Tool chain * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) * tools to provide nicer surface syntax and generate lisp syntax Document summarizing operators of interest: * http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/main.pdf Some differences: * separate operators for + on integers, reals * no 'nat' for now, indexing lists gives unknown value * a 'finite' predicate, no separate type * introduce a type for SMT-LIB 2.0 (same problem for maps) * finiteness inference * no set intervals * option types * subset of list operations