added split_paired_Ex to the implicit simpset
authoroheimb
Thu Jan 08 18:09:47 1998 +0100 (1998-01-08)
changeset 453674f7c556fd90
parent 4535 f24cebc299e4
child 4537 4e835bd9fada
added split_paired_Ex to the implicit simpset
src/HOL/thy_syntax.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/Traces.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Jan 08 18:09:07 1998 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Jan 08 18:09:47 1998 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4      \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     1.5      \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
     1.6        ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     1.7 -    \            ALLGOALS Asm_simp_tac]);\n\
     1.8 +    \            ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
     1.9      \val thy = thy\n";
    1.10  
    1.11  (*
     2.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Jan 08 18:09:07 1998 +0100
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Jan 08 18:09:47 1998 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  
     2.5  (* Has been removed from HOL-simpset, who knows why? *)
     2.6  Addsimps [Let_def];
     2.7 +Delsimps [split_paired_Ex];
     2.8  
     2.9  open reachable;
    2.10  
     3.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Thu Jan 08 18:09:07 1998 +0100
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Thu Jan 08 18:09:47 1998 +0100
     3.3 @@ -7,6 +7,7 @@
     3.4  *)   
     3.5  
     3.6  Delsimps (ex_simps @ all_simps);
     3.7 +Delsimps [split_paired_Ex];
     3.8  
     3.9  val exec_rws = [executions_def,is_exec_frag_def];
    3.10