This is an old revision of the document!


A PCRE internal error occured. This might be caused by a faulty plugin

====== 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: * {{:isabellemain.pdf|What's in Isabelle Main, October 14}} 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