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/UNITY/SubstAx.ML
changeset 5536 130f3d891fb2
parent 5479 5a5dfb0f0d7d
child 5544 96078cf5fd2c 
--- a/src/HOL/UNITY/SubstAx.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -267,7 +267,7 @@
 
 Goal "[| LeadsTo prg A A'; Stable prg B |] \
 \     ==> LeadsTo prg (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
 qed "PSP_stable2";
 
 Goalw [LeadsTo_def, Constrains_def]
@@ -278,7 +278,7 @@
 
 Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
 \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
 qed "PSP2";
 
 Goalw [Unless_def]
isabelle