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