removed introiff (cf. b09afce1e54f);
authorwenzelm
Mon, 27 Feb 2012 20:42:09 +0100
changeset 46719 61cd0ad6cd42
parent 46718 dfaf51de90ad
child 46720 9722171731af
removed introiff (cf. b09afce1e54f);
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