aboutsummaryrefslogtreecommitdiff
path: root/spartan/data/More_Types.thy
diff options
context:
space:
mode:
authorJosh Chen2020-05-27 22:16:42 +0200
committerJosh Chen2020-05-27 22:16:42 +0200
commitf12983b1b53c71fc416155ac4b7e2b11ed8ca9ef (patch)
treeaa8370faefd779bbdf45676e77001c25a4d3f5cc /spartan/data/More_Types.thy
parented41980ed5cee12d7c5eea2e40627e5a390a83f8 (diff)
change variable name in elim rules and fix small mistake
Diffstat (limited to '')
-rw-r--r--spartan/data/More_Types.thy3
1 files changed, 2 insertions, 1 deletions
diff --git a/spartan/data/More_Types.thy b/spartan/data/More_Types.thy
index f0cee6d..fecf378 100644
--- a/spartan/data/More_Types.thy
+++ b/spartan/data/More_Types.thy
@@ -1,9 +1,10 @@
+chapter \<open>Some standard types\<close>
+
theory More_Types
imports Spartan
begin
-
section \<open>Sum type\<close>
axiomatization