src/HOLCF/domain/theorems.ML
 changeset 8149 941afb897532 parent 7906 0576dad973b1 child 8438 b8389b4fca9c
1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:22:02 2000 +0100
1.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:23:41 2000 +0100
1.3 @@ -27,14 +27,6 @@
1.4  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf
1.5                                  | prems=> (cut_facts_tac prems 1)::tacsf);
1.7 -fun REPEAT_DETERM_UNTIL p tac =
1.8 -let fun drep st = if p st then Seq.single st
1.9 -                          else (case Seq.pull(tac st) of
1.10 -                                  None        => Seq.empty
1.11 -                                | Some(st',_) => drep st')
1.12 -in drep end;
1.13 -val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
1.14 -
1.15  local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
1.16  val kill_neq_tac = dtac trueI2 end;
1.17  fun case_UU_tac rews i v =      case_tac (v^"=UU") i THEN
1.18 @@ -131,7 +123,7 @@
1.19                                  rewrite_goals_tac axs_con_def,
1.20                                  dtac iso_swap 1,
1.21                                  simp_tac HOLCF_ss 1,
1.22 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
1.23 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
1.24              fun sum_tac [(_,args)]       [p]        =
1.25                                  prod_tac args THEN sum_rest_tac p
1.26              |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
1.27 @@ -159,7 +151,7 @@
1.28                                  else sum_tac cons (tl prems)])end;
1.29  val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
1.30                                  rtac casedist 1,
1.31 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
1.32 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
1.33  end;
1.35  local
1.36 @@ -197,7 +189,7 @@
1.37                        defined(%%(dis_name con)`%x_name)) [
1.38                                  rtac casedist 1,
1.39                                  contr_tac 1,
1.40 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac
1.41 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
1.42                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
1.43  in dis_stricts @ dis_defins @ dis_apps end;
1.45 @@ -237,7 +229,7 @@
1.46                          defined(%%(sel_of arg)`%x_name)) [
1.47                                  rtac casedist 1,
1.48                                  contr_tac 1,
1.49 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac
1.50 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac