src/HOL/Transitive_Closure.thy
changeset 26340 a85fe32e7b2f
parent 26271 e324f8918c98
child 26801 244184661a09
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:35 2008 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:38 2008 +0100
     1.3 @@ -618,18 +618,18 @@
     1.4  
     1.5  subsection {* Setup of transitivity reasoner *}
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9  
    1.10  structure Trancl_Tac = Trancl_Tac_Fun (
    1.11    struct
    1.12 -    val r_into_trancl = thm "trancl.r_into_trancl";
    1.13 -    val trancl_trans  = thm "trancl_trans";
    1.14 -    val rtrancl_refl = thm "rtrancl.rtrancl_refl";
    1.15 -    val r_into_rtrancl = thm "r_into_rtrancl";
    1.16 -    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    1.17 -    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    1.18 -    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
    1.19 -    val rtrancl_trans = thm "rtrancl_trans";
    1.20 +    val r_into_trancl = @{thm trancl.r_into_trancl};
    1.21 +    val trancl_trans  = @{thm trancl_trans};
    1.22 +    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    1.23 +    val r_into_rtrancl = @{thm r_into_rtrancl};
    1.24 +    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    1.25 +    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    1.26 +    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    1.27 +    val rtrancl_trans = @{thm rtrancl_trans};
    1.28  
    1.29    fun decomp (Trueprop $ t) =
    1.30      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    1.31 @@ -645,14 +645,14 @@
    1.32  
    1.33  structure Tranclp_Tac = Trancl_Tac_Fun (
    1.34    struct
    1.35 -    val r_into_trancl = thm "tranclp.r_into_trancl";
    1.36 -    val trancl_trans  = thm "tranclp_trans";
    1.37 -    val rtrancl_refl = thm "rtranclp.rtrancl_refl";
    1.38 -    val r_into_rtrancl = thm "r_into_rtranclp";
    1.39 -    val trancl_into_rtrancl = thm "tranclp_into_rtranclp";
    1.40 -    val rtrancl_trancl_trancl = thm "rtranclp_tranclp_tranclp";
    1.41 -    val trancl_rtrancl_trancl = thm "tranclp_rtranclp_tranclp";
    1.42 -    val rtrancl_trans = thm "rtranclp_trans";
    1.43 +    val r_into_trancl = @{thm tranclp.r_into_trancl};
    1.44 +    val trancl_trans  = @{thm tranclp_trans};
    1.45 +    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    1.46 +    val r_into_rtrancl = @{thm r_into_rtranclp};
    1.47 +    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    1.48 +    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    1.49 +    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    1.50 +    val rtrancl_trans = @{thm rtranclp_trans};
    1.51  
    1.52    fun decomp (Trueprop $ t) =
    1.53      let fun dec (rel $ a $ b) =
    1.54 @@ -665,13 +665,14 @@
    1.55      in dec t end;
    1.56  
    1.57    end);
    1.58 +*}
    1.59  
    1.60 -change_simpset (fn ss => ss
    1.61 -  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.62 -  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    1.63 -  addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    1.64 -  addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)));
    1.65 -
    1.66 +declaration {* fn _ =>
    1.67 +  Simplifier.map_ss (fn ss => ss
    1.68 +    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.69 +    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    1.70 +    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    1.71 +    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
    1.72  *}
    1.73  
    1.74  (* Optional methods *)