Fixed serializer for definitions using equality from Pure.
adbrucker/isabelle-hacks/master This commit looks good
Details
adbrucker/isabelle-hacks/master This commit looks good
Details
This commit is contained in:
parent
05741ac245
commit
faae943ad9
|
@ -39,6 +39,7 @@ to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
|
|||
|
||||
## [Unreleased]
|
||||
- Improved representation of IEEE reals
|
||||
- Fixed serializer for definitions using equality from Pure
|
||||
|
||||
## [1.0.0] - 2019-01-21
|
||||
- Initial release
|
||||
|
@ -706,7 +707,8 @@ structure Nano_Json_Serialize_Isar = struct
|
|||
val master_dir = Resources.master_directory thy
|
||||
val term = Thm.concl_of (Global_Theory.get_thm thy (json_const^"_def"))
|
||||
val json_term = case term of
|
||||
_ $ (_ $ json_term) => json_term
|
||||
Const (@{const_name "Pure.eq"}, _) $ _ $ json_term => json_term
|
||||
| _ $ (_ $ json_term) => json_term
|
||||
| _ => error ("Term structure not supported: "
|
||||
^(Sledgehammer_Util.hackish_string_of_term ctxt term))
|
||||
val json_string = Nano_Json_Serializer.serialize_term_pretty json_term
|
||||
|
|
Loading…
Reference in New Issue