equal
deleted
inserted
replaced
732 "specify realizers for primitive axioms / theorems, together with correctness proof" |
732 "specify realizers for primitive axioms / theorems, together with correctness proof" |
733 K.thy_decl |
733 K.thy_decl |
734 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
734 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
735 (fn xs => Toplevel.theory (fn thy => add_realizers |
735 (fn xs => Toplevel.theory (fn thy => add_realizers |
736 (map (fn (((a, vs), s1), s2) => |
736 (map (fn (((a, vs), s1), s2) => |
737 (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy))); |
737 (PureThy.get_thm thy (a, None), (vs, s1, s2))) xs) thy))); |
738 |
738 |
739 val realizabilityP = |
739 val realizabilityP = |
740 OuterSyntax.command "realizability" |
740 OuterSyntax.command "realizability" |
741 "add equations characterizing realizability" K.thy_decl |
741 "add equations characterizing realizability" K.thy_decl |
742 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
742 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
747 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
747 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
748 |
748 |
749 val extractP = |
749 val extractP = |
750 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
750 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
751 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
751 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
752 (fn thy => extract (map (apfst (PureThy.get_thm thy)) xs) thy))); |
752 (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair None)) xs) thy))); |
753 |
753 |
754 val parsers = [realizersP, realizabilityP, typeofP, extractP]; |
754 val parsers = [realizersP, realizabilityP, typeofP, extractP]; |
755 |
755 |
756 val setup = |
756 val setup = |
757 [ExtractionData.init, |
757 [ExtractionData.init, |