Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IOA/NTP/Correctness.ML
changeset 2638 6c6a44b5f757
parent 2513 d708d8cdc8e8 
--- a/src/HOL/IOA/NTP/Correctness.ML	Sat Feb 15 17:52:31 1997 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Sat Feb 15 17:55:11 1997 +0100
@@ -78,7 +78,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 addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
@@ -92,7 +92,7 @@
 by (forward_tac [inv2] 1);
 by (etac disjE 1);
 by (Asm_simp_tac 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (asm_simp_tac ss' 1);
 by (forward_tac [inv2] 1);
@@ -106,7 +106,7 @@
 
 by (case_tac "m = hd(sq(sen(s)))" 1);
 
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (Asm_full_simp_tac 1);
 by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
isabelle