forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
15e71fe189
|
@ -1010,8 +1010,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
|
||||||
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
||||||
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||||
(base_name')
|
(base_name')
|
||||||
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
|
||||||
(base_name' ^ " List.list")
|
|
||||||
val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
|
val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
|
||||||
val table_list = Symtab.dest tab
|
val table_list = Symtab.dest tab
|
||||||
fun get_instances_name_list _ [] = []
|
fun get_instances_name_list _ [] = []
|
||||||
|
@ -1028,13 +1026,7 @@ fun elaborate_instances_list thy isa_name _ _ _ =
|
||||||
end
|
end
|
||||||
val long_class_name = DOF_core.read_cid_global thy base_name'
|
val long_class_name = DOF_core.read_cid_global thy base_name'
|
||||||
val values_list = get_instances_name_list long_class_name table_list
|
val values_list = get_instances_name_list long_class_name table_list
|
||||||
val hol_list_terms_list =
|
in HOLogic.mk_list class_typ values_list end
|
||||||
fold
|
|
||||||
(fn x =>
|
|
||||||
fn y =>
|
|
||||||
Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
|
|
||||||
values_list (Const (@{const_name "Nil"}, class_list_typ))
|
|
||||||
in hol_list_terms_list end
|
|
||||||
|
|
||||||
fun declare_class_instances_annotation thy doc_class_name =
|
fun declare_class_instances_annotation thy doc_class_name =
|
||||||
let
|
let
|
||||||
|
|
|
@ -200,7 +200,10 @@ text\<open>Assertions must be true, hence the error:\<close>
|
||||||
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
||||||
|
|
||||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||||
assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||||
|
|
||||||
|
text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close>
|
||||||
|
text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
|
||||||
|
|
||||||
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||||
|
|
||||||
|
|
Reference in New Issue