equal
deleted
inserted
replaced
102 |
102 |
103 |
103 |
104 text{*This ML code does the inductions directly.*} |
104 text{*This ML code does the inductions directly.*} |
105 ML{* |
105 ML{* |
106 val ns_constrainsI = thm "ns_constrainsI"; |
106 val ns_constrainsI = thm "ns_constrainsI"; |
|
107 val impCE = thm "impCE"; |
107 |
108 |
108 fun ns_constrains_tac(cs,ss) i = |
109 fun ns_constrains_tac(cs,ss) i = |
109 SELECT_GOAL |
110 SELECT_GOAL |
110 (EVERY [REPEAT (etac Always_ConstrainsI 1), |
111 (EVERY [REPEAT (etac Always_ConstrainsI 1), |
111 REPEAT (resolve_tac [StableI, stableI, |
112 REPEAT (resolve_tac [StableI, stableI, |