# HG changeset patch
# User wenzelm
# Date 1330371729 -3600
# Node ID 61cd0ad6cd42f68fd07788f5d94222e9d4fb8c23
# Parent  dfaf51de90adf6df7c4f7ee31b674df2a3fcaa9d
removed introiff (cf. b09afce1e54f);

diff -r dfaf51de90ad -r 61cd0ad6cd42 src/Tools/WWW_Find/html_templates.ML
--- a/src/Tools/WWW_Find/html_templates.ML	Mon Feb 27 20:33:18 2012 +0100
+++ b/src/Tools/WWW_Find/html_templates.ML	Mon Feb 27 20:42:09 2012 +0100
@@ -93,14 +93,14 @@
 
 fun show_criterion (b, c) =
   let
-    fun prfx s = let
+    fun prfx s =
+      let
         val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
       in span (class c, v) end;
   in
     (case c of
       Find_Theorems.Name name => prfx ("name: " ^ quote name)
     | Find_Theorems.Intro => prfx "intro"
-    | Find_Theorems.IntroIff => prfx "introiff"
     | Find_Theorems.Elim => prfx "elim"
     | Find_Theorems.Dest => prfx "dest"
     | Find_Theorems.Solves => prfx "solves"
@@ -133,7 +133,7 @@
       [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
   end
 
-(*FIXME!?!*)
+(* FIXME!?! *)
 fun is_sorry thm =
   Thm.proof_of thm
   |> Proofterm.approximate_proof_body