equal
deleted
inserted
replaced
38 ); |
38 ); |
39 |
39 |
40 fun print_rules ctxt = |
40 fun print_rules ctxt = |
41 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
41 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
42 [Pretty.big_list "transitivity rules:" |
42 [Pretty.big_list "transitivity rules:" |
43 (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)), |
43 (map (Display.pretty_thm ctxt) (Item_Net.content trans)), |
44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
44 Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)] |
45 |> Pretty.chunks |> Pretty.writeln |
45 |> Pretty.chunks |> Pretty.writeln |
46 end; |
46 end; |
47 |
47 |
48 |
48 |
49 (* access calculation *) |
49 (* access calculation *) |