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.
clarified sym_del;
authorwenzelm
Thu, 06 Dec 2001 00:42:00 +0100
changeset 12402 cef751fff6b0
parent 12401 4363432ef0cd
child 12403 3e3bd3d449b5
clarified sym_del;
src/Pure/Isar/calculation.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/calculation.ML	Thu Dec 06 00:41:37 2001 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Dec 06 00:42:00 2001 +0100
@@ -102,9 +102,9 @@
 val trans_del_local = local_att (apfst o NetRules.delete);
 
 val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
-val sym_del_global = global_att (apsnd o Drule.del_rule);
+val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
 val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
-val sym_del_local = local_att (apsnd o Drule.del_rule);
+val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
 
 
 (* symmetry *)
isabelle