From c9a174bdbc7c6567bd0162785703e0e759760224 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 19 Jan 2019 08:23:18 +0000 Subject: [PATCH] Initial commit. --- Nano_JSON.thy | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 Nano_JSON.thy diff --git a/Nano_JSON.thy b/Nano_JSON.thy new file mode 100644 index 0000000..236bc2d --- /dev/null +++ b/Nano_JSON.thy @@ -0,0 +1,40 @@ +(*********************************************************************************** + * Copyright (c) 2019 Achim D. Brucker + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * SPDX-License-Identifier: BSD-2-Clause + * Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/ + * Dependencies: None (assert.thy is used for testing the theory but it is + * not required for providing the functionality of this hack) + ***********************************************************************************) + +chapter\An Import/Export of JSON-like Formats for Isabelle/HOL\ +theory + "Nano_JSON" +imports + Complex_Main + "Assert" (* Can be removed, after removing all assertions. *) +keywords +begin +end