equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Export and re-import of global proof terms\<close> |
12 subsection \<open>Export and re-import of global proof terms\<close> |
13 |
13 |
14 ML \<open> |
14 ML \<open> |
15 fun export_proof thm = |
15 fun export_proof thy thm = |
16 Proofterm.encode (Thm.clean_proof_of true thm); |
16 Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm); |
17 |
17 |
18 fun import_proof thy xml = |
18 fun import_proof thy xml = |
19 let |
19 let |
20 val prf = Proofterm.decode xml; |
20 val prf = Proofterm.decode (Sign.consts_of thy) xml; |
21 val (prf', _) = Proofterm.freeze_thaw_prf prf; |
21 val (prf', _) = Proofterm.freeze_thaw_prf prf; |
22 in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; |
22 in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; |
23 \<close> |
23 \<close> |
24 |
24 |
25 |
25 |
28 ML \<open>val thy1 = \<^theory>\<close> |
28 ML \<open>val thy1 = \<^theory>\<close> |
29 |
29 |
30 lemma ex: "A \<longrightarrow> A" .. |
30 lemma ex: "A \<longrightarrow> A" .. |
31 |
31 |
32 ML_val \<open> |
32 ML_val \<open> |
33 val xml = export_proof @{thm ex}; |
33 val xml = export_proof thy1 @{thm ex}; |
34 val thm = import_proof thy1 xml; |
34 val thm = import_proof thy1 xml; |
35 \<close> |
35 \<close> |
36 |
36 |
37 ML_val \<open> |
37 ML_val \<open> |
38 val xml = export_proof @{thm de_Morgan}; |
38 val xml = export_proof thy1 @{thm de_Morgan}; |
39 val thm = import_proof thy1 xml; |
39 val thm = import_proof thy1 xml; |
40 \<close> |
40 \<close> |
41 |
41 |
42 ML_val \<open> |
42 ML_val \<open> |
43 val xml = export_proof @{thm Drinker's_Principle}; |
43 val xml = export_proof thy1 @{thm Drinker's_Principle}; |
44 val thm = import_proof thy1 xml; |
44 val thm = import_proof thy1 xml; |
45 \<close> |
45 \<close> |
46 |
46 |
47 text \<open>Some fairly large proof:\<close> |
47 text \<open>Some fairly large proof:\<close> |
48 |
48 |
49 ML_val \<open> |
49 ML_val \<open> |
50 val xml = export_proof @{thm abs_less_iff}; |
50 val xml = export_proof thy1 @{thm abs_less_iff}; |
51 val thm = import_proof thy1 xml; |
51 val thm = import_proof thy1 xml; |
52 \<^assert> (size (YXML.string_of_body xml) > 1000000); |
52 \<^assert> (size (YXML.string_of_body xml) > 500000); |
53 \<close> |
53 \<close> |
54 |
54 |
55 end |
55 end |