i studied isabelle/isar implementation, isabelle/isar reference manual and the
isabelle cookbook.
what am i still doing wrong ?
structure Data = Proof_Data
(type T = term list
fun init _ = []);
val ctxt =
ProofContext.init_global @{theory} |>
Data.map (fn trms => @{term "x::int"}::trms);
Data.get ctxt;
Syntax.read_term ctxt "x + 1 = 2";
(* we get Free ("x", "'a") etc, but would expect ...
val it =
Const ("HOL.eq", "Int.int \<Rightarrow> Int.int \<Rightarrow>
HOL.bool") $
(Const ("Groups.plus_class.plus", "Int.int \<Rightarrow> Int.int
\<Rightarrow> Int.int") $
Free ("x", "Int.int") $ Const ("Groups.one_class.one", "Int.int")) $
(Const ("Int.number_class.number_of", "Int.int \<Rightarrow>
Int.int") $
(Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
(Const ("...", "Int.int \<Rightarrow> Int.int") $
Const ("Int.Pls...", "Int.int")))):
term
*)
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
