137 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
139 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
139 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
140 | _ => error "script.sml, doesnt find Substitute #2"; |
140 | _ => error "script.sml, doesnt find Substitute #2"; |
141 (* ERROR: caused by f2str f *) |
141 (* ERROR: caused by f2str f *) |
142 trace_rewrite:=true; |
142 trace_rewrite := false; |
143 |
143 |
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); |
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); |
145 trace_rewrite:=false; |
145 trace_rewrite:=false; |
146 (*Exception TYPE raised: |
146 (*Exception TYPE raised: |
147 Illegal type for constant "HOL.eq" :: "[real, bool] => bool" |
147 Illegal type for constant "HOL.eq" :: "[real, bool] => bool" |