293 val bool = Type ("bool",[]); (* 2002 Integ.int *) |
293 val bool = Type ("bool",[]); (* 2002 Integ.int *) |
294 val Trueprop = Const("Trueprop",bool-->prop); |
294 val Trueprop = Const("Trueprop",bool-->prop); |
295 fun mk_prop t = Trueprop $ t; |
295 fun mk_prop t = Trueprop $ t; |
296 val true_as_term = Const("True",bool); |
296 val true_as_term = Const("True",bool); |
297 val false_as_term = Const("False",bool); |
297 val false_as_term = Const("False",bool); |
298 val true_as_cterm = cterm_of HOL true_as_term; |
298 val true_as_cterm = cterm_of (theory "HOL") true_as_term; |
299 val false_as_cterm = cterm_of HOL false_as_term; |
299 val false_as_cterm = cterm_of (theory "HOL") false_as_term; |
300 |
300 |
301 infixr 5 -->; (*2002 /Pure/term.ML *) |
301 infixr 5 -->; (*2002 /Pure/term.ML *) |
302 infixr --->; (*2002 /Pure/term.ML *) |
302 infixr --->; (*2002 /Pure/term.ML *) |
303 fun S --> T = Type("fun",[S,T]); (*2002 /Pure/term.ML *) |
303 fun S --> T = Type("fun",[S,T]); (*2002 /Pure/term.ML *) |
304 val op ---> = foldr (op -->); (*2002 /Pure/term.ML *) |
304 val op ---> = foldr (op -->); (*2002 /Pure/term.ML *) |
1253 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1253 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1254 *** Free ( R, RealDef.real) |
1254 *** Free ( R, RealDef.real) |
1255 *** Free ( R, RealDef.real) *) |
1255 *** Free ( R, RealDef.real) *) |
1256 |
1256 |
1257 (*version for testing local to theories*) |
1257 (*version for testing local to theories*) |
1258 fun str2t thy str = (term_of o the o (parse thy )) str; |
1258 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1259 |
1259 fun str2term str = (term_of o the o (parse (theory "Isac"))) str; |
1260 fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str; |
|
1261 fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str; |
|
1262 fun strs2terms ss = map str2term ss; |
1260 fun strs2terms ss = map str2term ss; |
|
1261 fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str; |
1263 |
1262 |
1264 (*+ makes a substitution from the output of Pattern.match +*) |
1263 (*+ makes a substitution from the output of Pattern.match +*) |
1265 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) |
1264 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) |
1266 fun mk_subs (subs: ((string * int) * (Term.typ * Term.term)) list) = |
1265 fun mk_subs (subs: ((string * int) * (Term.typ * Term.term)) list) = |
1267 let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in |
1266 let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in |