Fixed a bug where the simplifier would hang on
lemma "f a = M { nat j |j. 0 <= j & j < f b}"
pre_decomp/pre_tac no longer split terms that contain (non-locally) bound
variables (e.g., "nat j" in the above example).
(* Title: HOLCF/IOA/Storage/ROOT.ML
ID: $Id$
Author: Olaf Mueller
Memory storage case study.
*)
goals_limit := 1;
time_use_thy "Correctness";