--- a/src/HOL/Orderings.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Orderings.thy Sat Oct 17 14:43:18 2009 +0200
@@ -339,18 +339,18 @@
(* exclude numeric types: linear arithmetic subsumes transitivity *)
let val T = type_of t
in
- T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
+ T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
end;
- fun rel (bin_op $ t1 $ t2) =
+ fun rel (bin_op $ t1 $ t2) =
if excluded t1 then NONE
else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
else NONE
- | rel _ = NONE;
- fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
- of NONE => NONE
- | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
+ | rel _ = NONE;
+ fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
+ of NONE => NONE
+ | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
| dec x = rel x;
in dec t end
| decomp thy _ = NONE;