equal
deleted
inserted
replaced
97 |
97 |
98 (* simpset *) |
98 (* simpset *) |
99 |
99 |
100 local |
100 local |
101 val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} |
101 val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} |
102 val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2} |
102 val antisym_le2 = mk_meta_eq @{thm order_class.antisym_conv2} |
103 val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1} |
103 val antisym_less1 = mk_meta_eq @{thm order_class.antisym_conv1} |
104 val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} |
104 val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} |
105 |
105 |
106 fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
106 fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
107 fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
107 fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
108 | dest_binop t = raise TERM ("dest_binop", [t]) |
108 | dest_binop t = raise TERM ("dest_binop", [t]) |