equal
deleted
inserted
replaced
240 fun rewrite_terms_ thy ord erls equs t = |
240 fun rewrite_terms_ thy ord erls equs t = |
241 let |
241 let |
242 fun rew_ (t', asm') [] _ = (t', asm') |
242 fun rew_ (t', asm') [] _ = (t', asm') |
243 | rew_ (t', asm') (rules as r::rs) t = |
243 | rew_ (t', asm') (rules as r::rs) t = |
244 let |
244 let |
245 val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (TermC.Trueprop $ r) t |
245 val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t |
246 in |
246 in |
247 if rew |
247 if rew |
248 then rew_ (t'', asm' @ asm'') rules t'' |
248 then rew_ (t'', asm' @ asm'') rules t'' |
249 else rew_ (t', asm') rs t' |
249 else rew_ (t', asm') rs t' |
250 end |
250 end |
269 fun mk_thm thy str = |
269 fun mk_thm thy str = |
270 let |
270 let |
271 val t = (Thm.term_of o the o (TermC.parse thy)) str |
271 val t = (Thm.term_of o the o (TermC.parse thy)) str |
272 val t' = case t of |
272 val t' = case t of |
273 Const ("Pure.imp", _) $ _ $ _ => t |
273 Const ("Pure.imp", _) $ _ $ _ => t |
274 | _ => TermC.Trueprop $ t |
274 | _ => HOLogic.Trueprop $ t |
275 in Thm.make_thm (Thm.global_cterm_of thy t') end; |
275 in Thm.make_thm (Thm.global_cterm_of thy t') end; |
276 |
276 |
277 (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *) |
277 (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *) |
278 fun convert_metaview_to_thmid thy thmid = |
278 fun convert_metaview_to_thmid thy thmid = |
279 let val thmid' = case thmid of |
279 let val thmid' = case thmid of |