observe standard header format;
authorwenzelm
Thu Mar 03 15:36:54 2011 +0100 (2011-03-03)
changeset 41883392364739e5d
parent 41882 ae8d62656392
child 41884 335895ffbd94
observe standard header format;
src/Tools/case_product.ML
     1.1 --- a/src/Tools/case_product.ML	Thu Mar 03 15:19:20 2011 +0100
     1.2 +++ b/src/Tools/case_product.ML	Thu Mar 03 15:36:54 2011 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4 -(*   Title: case_product.ML
     1.5 -     Author: Lars Noschinski
     1.6 +(*  Title:      Tools/case_product.ML
     1.7 +    Author:     Lars Noschinski, TU Muenchen
     1.8  
     1.9  Combines two case rules into a single one.
    1.10  
    1.11 @@ -9,8 +9,7 @@
    1.12  *)
    1.13  
    1.14  signature CASE_PRODUCT =
    1.15 -  sig
    1.16 -
    1.17 +sig
    1.18    val combine: Proof.context -> thm -> thm -> thm
    1.19    val combine_annotated: Proof.context -> thm -> thm -> thm
    1.20    val setup: theory -> theory
    1.21 @@ -104,7 +103,8 @@
    1.22  
    1.23  (* Attribute setup *)
    1.24  
    1.25 -val case_prod_attr = let
    1.26 +val case_prod_attr =
    1.27 +  let
    1.28      fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
    1.29    in
    1.30      Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>