src/HOL/Statespace/distinct_tree_prover.ML
changeset 39159 0dec18004e75
parent 38864 4abe644fcea5
child 42361 23f352990944
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -23,18 +23,19 @@
     1.4  
     1.5  structure DistinctTreeProver : DISTINCT_TREE_PROVER =
     1.6  struct
     1.7 -val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
     1.8 -val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
     1.9 +
    1.10 +val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left};
    1.11 +val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right};
    1.12  
    1.13 -val distinct_left = thm "DistinctTreeProver.distinct_left";
    1.14 -val distinct_right = thm "DistinctTreeProver.distinct_right";
    1.15 -val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
    1.16 -val in_set_root = thm "DistinctTreeProver.in_set_root";
    1.17 -val in_set_left = thm "DistinctTreeProver.in_set_left";
    1.18 -val in_set_right = thm "DistinctTreeProver.in_set_right";
    1.19 +val distinct_left = @{thm DistinctTreeProver.distinct_left};
    1.20 +val distinct_right = @{thm DistinctTreeProver.distinct_right};
    1.21 +val distinct_left_right = @{thm DistinctTreeProver.distinct_left_right};
    1.22 +val in_set_root = @{thm DistinctTreeProver.in_set_root};
    1.23 +val in_set_left = @{thm DistinctTreeProver.in_set_left};
    1.24 +val in_set_right = @{thm DistinctTreeProver.in_set_right};
    1.25  
    1.26 -val swap_neq = thm "DistinctTreeProver.swap_neq";
    1.27 -val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
    1.28 +val swap_neq = @{thm DistinctTreeProver.swap_neq};
    1.29 +val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
    1.30  
    1.31  datatype Direction = Left | Right 
    1.32  
    1.33 @@ -273,9 +274,9 @@
    1.34    end  
    1.35  
    1.36  
    1.37 -val delete_root = thm "DistinctTreeProver.delete_root";
    1.38 -val delete_left = thm "DistinctTreeProver.delete_left";
    1.39 -val delete_right = thm "DistinctTreeProver.delete_right";
    1.40 +val delete_root = @{thm DistinctTreeProver.delete_root};
    1.41 +val delete_left = @{thm DistinctTreeProver.delete_left};
    1.42 +val delete_right = @{thm DistinctTreeProver.delete_right};
    1.43  
    1.44  fun deleteProver dist_thm [] = delete_root OF [dist_thm]
    1.45    | deleteProver dist_thm (p::ps) =
    1.46 @@ -286,10 +287,10 @@
    1.47         val del = deleteProver dist_thm' ps;
    1.48       in discharge [dist_thm, del] del_rule end;
    1.49  
    1.50 -val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
    1.51 -val subtract_Node = thm "DistinctTreeProver.subtract_Node";
    1.52 -val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
    1.53 -val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
    1.54 +val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
    1.55 +val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
    1.56 +val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
    1.57 +val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
    1.58  
    1.59  local
    1.60    val (alpha,v) = 
    1.61 @@ -320,7 +321,7 @@
    1.62      in discharge [del_tree, sub_l, sub_r] subtract_Node end
    1.63  end
    1.64  
    1.65 -val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
    1.66 +val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
    1.67  fun distinct_implProver dist_thm ct =
    1.68    let
    1.69      val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;