Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed unsafe_addss to addss
authoroheimb
Fri, 16 May 1997 17:14:55 +0200
changeset 3221 90211fa9ee7e
parent 3220 47d2cf09b3d8
child 3222 726a9b069947
renamed unsafe_addss to addss
src/HOLCF/IMP/Denotational.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/NTP/Correctness.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IMP/Denotational.ML	Fri May 16 16:14:58 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Fri May 16 17:14:55 1997 +0200
@@ -32,9 +32,9 @@
 by (com.induct_tac "c" 1);
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
-  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
+  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
- by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
+ by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
 by (Simp_tac 1);
 br fix_ind 1;
   by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
@@ -42,7 +42,7 @@
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (safe_tac HOL_cs);
   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
+ by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
 qed_spec_mp "D_implies_eval";
 
 
--- a/src/HOLCF/IOA/NTP/Correctness.ML	Fri May 16 16:14:58 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML	Fri May 16 17:14:55 1997 +0200
@@ -77,7 +77,7 @@
 by (Action.action.induct_tac "a"  1);
 by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
 by (forward_tac [inv4] 1);
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
@@ -91,7 +91,7 @@
 by (forward_tac [inv2] 1);
 by (etac disjE 1);
 by (Asm_simp_tac 1);
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (asm_simp_tac ss' 1);
 by (forward_tac [inv2] 1);
@@ -105,7 +105,7 @@
 
 by (case_tac "m = hd(sq(sen(s)))" 1);
 
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (Asm_full_simp_tac 1);
 by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
isabelle