Hope there is somebody who needs not dig in the code to answer this
question ...
How can we produce specific patterns (some variables of a term should
become Free, some Var), for instance:
(term_of o the o (parse thy)) "matches (?a + ?b * bdv^2 = (0::real)) equ";
val it =
Const ("Tools.matches", "[bool, bool] => bool") $
(Const ("op =", "[RealDef.real, RealDef.real] => bool") $
(Const
("op +",
"[RealDef.real, RealDef.real] => RealDef.real") $
Var (("a", 0), "RealDef.real") $
(Const
("op *",
"[RealDef.real, RealDef.real] => RealDef.real")
$ Var (("b", 0), "RealDef.real") $
(Const
("Nat.power",
"[RealDef.real, nat] => RealDef.real") $
Free ("bdv", "RealDef.real") $
Free ("2", "nat")))) $ Free ("0", "RealDef.real")) $
Free ("equ", "bool") : Term.term
The above is from an outdated Isabelle version --- what are the
recommendations to produce specific patterns nowadays ?
Walther
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
