diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Natural.ML --- a/src/HOL/IMPP/Natural.ML Sat Sep 17 19:17:35 2005 +0200 +++ b/src/HOL/IMPP/Natural.ML Sat Sep 17 20:14:30 2005 +0200 @@ -4,21 +4,8 @@ Copyright 1999 TUM *) -open Natural; - -AddIs evalc.intrs; -AddIs evaln.intrs; - -val evalc_elim_cases = map evalc.mk_cases - [" -c-> t", " -c-> t", " -c-> t", - " -c-> t"," -c-> t", - " -c-> s1", " -c-> s1"]; -val evaln_elim_cases = map evaln.mk_cases - [" -n-> t", " -n-> t", " -n-> t", - " -n-> t"," -n-> t", - " -n-> s1", " -n-> s1"]; -val evalc_WHILE_case = evalc.mk_cases " -c-> t"; -val evaln_WHILE_case = evaln.mk_cases " -n-> t"; +AddIs evalc.intros; +AddIs evaln.intros; AddSEs evalc_elim_cases; AddSEs evaln_elim_cases; @@ -33,7 +20,7 @@ Goal " -n-> t ==> -c-> t"; by (etac evaln.induct 1); -by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); +by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac)); qed "evaln_evalc"; Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; @@ -46,7 +33,7 @@ Goal " -n-> t ==> !m. n<=m --> -m-> t"; by (etac evaln.induct 1); by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1])); -by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac)); +by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac)); qed_spec_mp "evaln_nonstrict"; Goal " -n-> s' ==> -Suc n-> s'"; @@ -64,7 +51,7 @@ by (etac evalc.induct 1); by (ALLGOALS (REPEAT o etac exE)); by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]])); -by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac)); +by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac)); qed "evalc_evaln"; Goal " -c-> t = (? n. -n-> t)";