adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: add license header text 

These two files were @TAG-ged but without copyright header text.
This commit is contained in:
Japheth Lim 2018-09-26 15:37:59 +10:00
parent e968766e12
commit a8129d0695
2 changed files with 18 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
lib/Insulin.thy
View File

@ -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:

10
lib/ShowTypes.thy
View File

@ -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.
*