merged

import constant folding theory into IMP

make syntax ambiguity warnings a config option

add lemmas INF_image, SUP_image

declare {INF,SUP}_empty [simp]

rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)

standard theorem naming scheme: complex_eqI, complex_eq_iff

moved division ring stuff from Rings.thy to Fields.thy

Library/Product_ord: wellorder instance for products

modernized file proof_checker.ML;

tuned thm_of_proof: build lookup table within closure;

added Reconstruct.proof_of convenience;

ship message in one piece;

misc tuning -- eliminated old-fashioned rep_thm;

modernized strcture Proof_Checker;

less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;

updated imports;

proper signature;

made SML/NJ happy;

slightly more uniform messages;

avoid pointless completion of illegal control commands;

removed old expand_fun_eq

fixed index entry

removed old recdef and types usage

merged

extended user-level attribute case_names with names for case hypotheses

infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names

workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;

updated version information;

fixed document;