equal
deleted
inserted
replaced
556 |
556 |
557 (* add method *) |
557 (* add method *) |
558 |
558 |
559 fun method_setup ((name, txt, cmt), comment_ignore) = |
559 fun method_setup ((name, txt, cmt), comment_ignore) = |
560 Context.use_let |
560 Context.use_let |
561 "val method: bstring * (Args.src -> Proof.context -> Proof.method) * string" |
561 "val thm = PureThy.get_thm_closure (Context.the_context ());\n\ |
|
562 \val thms = PureThy.get_thms_closure (Context.the_context ());\n\ |
|
563 \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string" |
562 "PureIsar.Method.add_method method" |
564 "PureIsar.Method.add_method method" |
563 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"); |
565 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"); |
564 |
566 |
565 |
567 |
566 (* add_oracle *) |
568 (* add_oracle *) |