isabelle: src/HOLCF/Porder0.ML@9e125b675253 (annotated)

2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	1
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	2	(* legacy ML bindings *)
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	3
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	4	val refl_less = thm "refl_less";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	5	val antisym_less = thm "antisym_less";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	6	val trans_less = thm "trans_less";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	7	val minimal2UU = thm "minimal2UU";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	8	val antisym_less_inverse = thm "antisym_less_inverse";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	9	val box_less = thm "box_less";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	10	val po_eq_conv = thm "po_eq_conv";