Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update DOF manual meta-types as types section 

Types of the implementation language inside the HOL type system
are now represented as datatypes and not just abstract types
This commit is contained in:
Nicolas Méric 2022-03-28 18:49:03 +02:00
parent 444d6d077c
commit 9cd5323063
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -993,8 +993,8 @@ text\<open>
entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or
\<^ML_type>\<open>thm\<close>, we represent the types of the implementation language
\<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of
these types. They are just declared abstract types,
``inhabited'' by special constant symbols carrying strings, for
these types. They are just types declared in HOL,
which are ``inhabited'' by special constant symbols carrying strings, for
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
% TODO:
% Update meta-types implementation explanation to the new implementation