equal
deleted
inserted
replaced
171 before_qed: Method.text option, 
171 before_qed: Method.text option, 
172 after_qed: 
172 after_qed: 
173 (context * thm list list > state > state) * 
173 (context * thm list list > state > state) * 
174 (context * thm list list > context > context)}; 
174 (context * thm list list > context > context)}; 
175 
175 

176 val _ = 

177 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state => 

178 Pretty.to_polyml (Pretty.str "<Proof.state>")); 

179 
176 fun make_goal (statement, using, goal, before_qed, after_qed) = 
180 fun make_goal (statement, using, goal, before_qed, after_qed) = 
177 Goal {statement = statement, using = using, goal = goal, 
181 Goal {statement = statement, using = using, goal = goal, 
178 before_qed = before_qed, after_qed = after_qed}; 
182 before_qed = before_qed, after_qed = after_qed}; 
179 
183 
180 fun make_node (context, facts, mode, goal) = 
184 fun make_node (context, facts, mode, goal) = 