equal
deleted
inserted
replaced
337 then rewrite_rule [eqn'] (Thm.transfer thy th) |
337 then rewrite_rule [eqn'] (Thm.transfer thy th) |
338 else th |
338 else th |
339 end) |
339 end) |
340 in add_preprocessor prep end; |
340 in add_preprocessor prep end; |
341 |
341 |
342 val _ = Context.add_setup |
342 val _ = Context.>> |
343 (let |
343 (let |
344 fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); |
344 fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); |
345 in |
345 in |
346 Code.add_attribute ("unfold", Scan.succeed (mk_attribute |
346 Code.add_attribute ("unfold", Scan.succeed (mk_attribute |
347 (fn thm => add_unfold thm #> Code.add_inline thm))) |
347 (fn thm => add_unfold thm #> Code.add_inline thm))) |
784 p module')) |
784 p module')) |
785 | SOME (_, module'', _) => |
785 | SOME (_, module'', _) => |
786 (add_edge (node_id, dep) gr'', p module'')) |
786 (add_edge (node_id, dep) gr'', p module'')) |
787 end); |
787 end); |
788 |
788 |
789 val _ = Context.add_setup |
789 val _ = Context.>> |
790 (add_codegen "default" default_codegen #> |
790 (add_codegen "default" default_codegen #> |
791 add_tycodegen "default" default_tycodegen); |
791 add_tycodegen "default" default_tycodegen); |
792 |
792 |
793 |
793 |
794 fun mk_tuple [p] = p |
794 fun mk_tuple [p] = p |
1024 if int andalso !auto_quickcheck andalso not (!Toplevel.quiet) |
1024 if int andalso !auto_quickcheck andalso not (!Toplevel.quiet) |
1025 then test () |
1025 then test () |
1026 else state |
1026 else state |
1027 end; |
1027 end; |
1028 |
1028 |
1029 val _ = Context.add_setup |
1029 val _ = Context.>> |
1030 (Context.theory_map (Specification.add_theorem_hook test_goal')); |
1030 (Context.theory_map (Specification.add_theorem_hook test_goal')); |
1031 |
1031 |
1032 |
1032 |
1033 (**** Evaluator for terms ****) |
1033 (**** Evaluator for terms ****) |
1034 |
1034 |
1076 |
1076 |
1077 fun evaluation_conv ct = |
1077 fun evaluation_conv ct = |
1078 let val {thy, t, ...} = rep_cterm ct |
1078 let val {thy, t, ...} = rep_cterm ct |
1079 in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end; |
1079 in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end; |
1080 |
1080 |
1081 val _ = Context.add_setup |
1081 val _ = Context.>> |
1082 (Theory.add_oracle ("evaluation", evaluation_oracle)); |
1082 (Theory.add_oracle ("evaluation", evaluation_oracle)); |
1083 |
1083 |
1084 |
1084 |
1085 (**** Interface ****) |
1085 (**** Interface ****) |
1086 |
1086 |