src/Provers/simplifier.ML
changeset 146 dbee71d43339
parent 88 9df4dfedee01
child 217 c972c57e7762
equal deleted inserted replaced
145:422197c5a078 146:dbee71d43339
   154                thm)
   154                thm)
   155       and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
   155       and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
   156       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
   156       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
   157       and simp_loop_tac i = Tactic(simp_loop i)
   157       and simp_loop_tac i = Tactic(simp_loop i)
   158 
   158 
   159   in fn i => COND (has_fewer_prems 0) no_tac (simp_loop_tac i) end;
   159   in fn i => COND (has_fewer_prems 1) no_tac (simp_loop_tac i) end;
   160 
   160 
   161 fun asm_simp_tac ss =
   161 fun asm_simp_tac ss =
   162       METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
   162       METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
   163 
   163 
   164 fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
   164 fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);