From a8129d0695966079669d2f662d1c821c59eb10d4 Mon Sep 17 00:00:00 2001
From: Japheth Lim <Japheth.Lim@data61.csiro.au>
Date: Wed, 26 Sep 2018 15:37:59 +1000
Subject: [PATCH] lib: add license header text

These two files were @TAG-ged but without copyright header text.
---
 lib/Insulin.thy   | 10 +++++++++-
 lib/ShowTypes.thy | 10 +++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/lib/Insulin.thy b/lib/Insulin.thy
index c61900e79..23672d65b 100644
--- a/lib/Insulin.thy
+++ b/lib/Insulin.thy
@@ -1,6 +1,14 @@
 (*
- * @TAG(NICTA_BSD)
+ * Copyright 2016, NICTA
  *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+(*
  * Insulin.thy: regulate sugar in terms, thms and proof goals.
  *
  * Usage:
diff --git a/lib/ShowTypes.thy b/lib/ShowTypes.thy
index 253cdb2c3..11f470b9b 100644
--- a/lib/ShowTypes.thy
+++ b/lib/ShowTypes.thy
@@ -1,6 +1,14 @@
 (*
- * @TAG(NICTA_BSD)
+ * Copyright 2016, NICTA
  *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+(*
  * ShowTypes: show "hidden" type constraints in terms.
  * This is a simple utility around Sledgehammer's type annotation code.
  *