1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory BuildRefineCache 12imports Main 13begin 14 15ML {* 16 17(* needed to generate a proof cache *) 18proofs := 1; 19DupSkip.record_proofs := true; 20quick_and_dirty := true; 21 22tracing "Building refinement image using ROOT.ML"; 23 24use "ROOT.ML"; 25 26*} 27 28ML {* 29 30tracing "Synching proof cache"; 31 32DupSkip.sync_cache @{theory Refine}; 33 34tracing "Dumping proof cache"; 35 36let 37 val xml = XML_Syntax.xml_forest_of_cache (! DupSkip.the_cache); 38in 39 File.open_output (XML_Syntax.output_forest xml) (Path.basic "proof_cache.xml") 40end; 41 42*} 43 44end 45