updated for latest Blast_tac, which treats equality differently
authorpaulson
Wed Dec 03 11:00:24 1997 +0100 (1997-12-03)
changeset 4353d565d2197a5f
parent 4352 7ac9f3e8a97d
child 4354 7f4da01bdf0e
updated for latest Blast_tac, which treats equality differently
src/HOL/ex/MT.ML
src/HOL/ex/cla.ML
     1.1 --- a/src/HOL/ex/MT.ML	Wed Dec 03 10:52:17 1997 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Dec 03 11:00:24 1997 +0100
     1.3 @@ -418,7 +418,7 @@
     1.4  fun elab_e_elim_tac p = 
     1.5    ( (rtac elab_elim 1) THEN 
     1.6      (resolve_tac p 1) THEN 
     1.7 -    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
     1.8 +    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
     1.9    );
    1.10  
    1.11  val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
     2.1 --- a/src/HOL/ex/cla.ML	Wed Dec 03 10:52:17 1997 +0100
     2.2 +++ b/src/HOL/ex/cla.ML	Wed Dec 03 11:00:24 1997 +0100
     2.3 @@ -386,7 +386,7 @@
     2.4  by (assume_tac 1);
     2.5  by (res_inst_tac [("x","b")] allE 1);
     2.6  by (assume_tac 1);
     2.7 -by (Blast_tac 1);
     2.8 +by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
     2.9  result();
    2.10  
    2.11  writeln"Problem 50";