--- a/src/Pure/thm.ML Fri Jul 18 13:36:03 1997 +0200
+++ b/src/Pure/thm.ML Fri Jul 18 13:36:43 1997 +0200
@@ -627,7 +627,9 @@
end;
(*Implication introduction
- A |- B
+ [A]
+ :
+ B
-------
A ==> B
*)
@@ -860,9 +862,9 @@
end;
(*The combination rule
- f==g t==u
- ------------
- f(t)==g(u)
+ f == g t == u
+ --------------
+ f(t) == g(u)
*)
fun combination th1 th2 =
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
@@ -896,9 +898,9 @@
(* Equality introduction
- A==>B B==>A
- --------------
- A==B
+ A ==> B B ==> A
+ ----------------
+ A == B
*)
fun equal_intr th1 th2 =
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1,
@@ -923,7 +925,7 @@
(*The equal propositions rule
- A==B A
+ A == B A
---------
B
*)
@@ -1423,7 +1425,7 @@
exception SIMPLIFIER of string * thm;
fun prtm a sign t = (writeln a; writeln (Sign.string_of_term sign t));
-fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t));
+fun prtm_warning a sign t = (warning a; warning (Sign.string_of_term sign t));
val trace_simp = ref false;