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.
record_split_name;
authorwenzelm
Wed, 21 Oct 1998 13:29:01 +0200
changeset 5706 21706a735c8d
parent 5705 56f2030c46c6
child 5707 b0e631634b5a
record_split_name;
src/HOL/UNITY/Client.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/Handshake.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/Lift.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/Mutex.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Client.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Client.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -19,7 +19,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [Cli_prg_def RS def_prg_Init];
 program_defs_ref := [Cli_prg_def];
--- a/src/HOL/UNITY/Comp.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Delsimps [split_paired_All];
 
--- a/src/HOL/UNITY/Handshake.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
 program_defs_ref := [F_def, G_def];
--- a/src/HOL/UNITY/Lift.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -12,7 +12,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Delsimps [split_paired_All];
 
--- a/src/HOL/UNITY/Mutex.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -7,7 +7,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [Mprg_def RS def_prg_Init];
 program_defs_ref := [Mprg_def];
isabelle