# HG changeset patch
# User kleing
# Date 1101879020 -3600
# Node ID 440687010501ee50fcb827270c0434b1c08fd2b0
# Parent  0a60f15c2d7a73243c824012029c9fe2854c0084
added antiquotations @{lhs thm} and @{rhs thm}

diff -r 0a60f15c2d7a -r 440687010501 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed Dec 01 04:11:15 2004 +0100
+++ b/src/Pure/Isar/isar_output.ML	Wed Dec 01 06:30:20 2004 +0100
@@ -324,6 +324,22 @@
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
 
+fun lhs_of (Const ("==",_) $ t $ _) = t
+  | lhs_of (Const ("Trueprop",_) $ t) = lhs_of t
+  | lhs_of (Const ("==>",_) $ _ $ t) = lhs_of t
+  | lhs_of (_ $ t $ _) = t
+  | lhs_of _ = error ("Binary operator expected")
+
+fun pretty_lhs ctxt = pretty_term ctxt o lhs_of o Thm.prop_of;
+
+fun rhs_of (Const ("==",_) $ _ $ t) = t
+  | rhs_of (Const ("Trueprop",_) $ t) = rhs_of t
+  | rhs_of (Const ("==>",_) $ _ $ t) = rhs_of t
+  | rhs_of (_ $ _ $ t) = t
+  | rhs_of _ = error ("Binary operator expected")
+
+fun pretty_rhs ctxt = pretty_term ctxt o rhs_of o Thm.prop_of;
+
 fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
   Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
 
@@ -345,6 +361,8 @@
 
 val _ = add_commands
  [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
+  ("lhs", args Attrib.local_thmss (output_seq_with pretty_lhs)),
+  ("rhs", args Attrib.local_thmss (output_seq_with pretty_rhs)),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
   ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),