Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
Proofterm.approximate_proof_body;
authorwenzelm
Wed, 25 Mar 2009 16:54:49 +0100
changeset 3071815041c7e51e4
parent 30717 465093aa5844
child 30719 21c20c7d1932
Proofterm.approximate_proof_body;
src/Pure/Proof/extraction.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/xml_syntax.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:17 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Mar 25 16:54:49 2009 +0100
     1.3 @@ -568,7 +568,7 @@
     1.4                        (proof_combt
     1.5                           (PThm (serial (),
     1.6                            ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
     1.7 -                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
     1.8 +                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
     1.9                        (map (get_var_type corr_prop) (vfs_of prop))
    1.10                    in
    1.11                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
    1.12 @@ -679,7 +679,7 @@
    1.13                        (proof_combt
    1.14                          (PThm (serial (),
    1.15                           ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.16 -                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.17 +                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
    1.18                        (map (get_var_type corr_prop) (vfs_of prop));
    1.19                    in
    1.20                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',

     2.1 --- a/src/Pure/Tools/xml_syntax.ML	Wed Mar 25 16:54:17 2009 +0100
     2.2 +++ b/src/Pure/Tools/xml_syntax.ML	Wed Mar 25 16:54:49 2009 +0100
     2.3 @@ -158,7 +158,7 @@
     2.4    | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
     2.5        (* FIXME? *)
     2.6        PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
     2.7 -        Future.value (Proofterm.make_proof_body MinProof)))
     2.8 +        Future.value (Proofterm.approximate_proof_body MinProof)))
     2.9    | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
    2.10        PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
    2.11    | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
wneuper/isa