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.
addsimprocs [record_simproc];
authorwenzelm
Sat, 25 Mar 2000 13:00:44 +0100
changeset 8576 142065da303d
parent 8575 7d79d2473b5e
child 8577 4a3cdf01531b
addsimprocs [record_simproc];
src/HOL/Hoare/Hoare.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Hoare/Hoare.ML	Sat Mar 25 12:59:31 2000 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Sat Mar 25 13:00:44 2000 +0100
@@ -163,7 +163,7 @@
           (EVERY [rtac subsetI i, 
                   rtac CollectI i,
                   dtac CollectD i,
-                  (TRY(split_all_tac i)) THEN_MAYBE 
+                  (TRY(split_all_tac i)) THEN_MAYBE
                   ((rename_tac var_string i) THEN
                    (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
       end;
@@ -179,7 +179,8 @@
 fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
 
 fun BasicSimpTac tac =
-  simp_tac (HOL_basic_ss addsimps [mem_Collect_eq,split])
+  simp_tac
+    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
   THEN_MAYBE' MaxSimpTac tac;
 
 (** HoareRuleTac **)
@@ -217,4 +218,4 @@
 
 val hoare_setup =
  [Method.add_methods
-  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];
+  [("hoare_vcg", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];
isabelle