--- a/src/Tools/case_product.ML Thu Mar 03 15:19:20 2011 +0100
+++ b/src/Tools/case_product.ML Thu Mar 03 15:36:54 2011 +0100
@@ -1,5 +1,5 @@
-(* Title: case_product.ML
- Author: Lars Noschinski
+(* Title: Tools/case_product.ML
+ Author: Lars Noschinski, TU Muenchen
Combines two case rules into a single one.
@@ -9,8 +9,7 @@
*)
signature CASE_PRODUCT =
- sig
-
+sig
val combine: Proof.context -> thm -> thm -> thm
val combine_annotated: Proof.context -> thm -> thm -> thm
val setup: theory -> theory
@@ -104,7 +103,8 @@
(* Attribute setup *)
-val case_prod_attr = let
+val case_prod_attr =
+ let
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
in
Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>