added thy_switch kind;
authorwenzelm
Tue, 27 Jul 1999 21:58:59 +0200
changeset 7104 247e4247b64e
parent 7103 1c44df10a7bc
child 7105 dcd7ac72f1e7
added thy_switch kind;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:39 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:59 1999 +0200
@@ -22,6 +22,7 @@
       val control: string
       val diag: string
       val thy_begin: string
+      val thy_switch: string
       val thy_end: string
       val thy_heading: string
       val thy_decl: string
@@ -68,6 +69,7 @@
   val control = "control";
   val diag = "diag";
   val thy_begin = "theory-begin";
+  val thy_switch = "theory-switch";
   val thy_end = "theory-end";
   val thy_heading = "theory-heading";
   val thy_decl = "theory-decl";
@@ -81,8 +83,8 @@
   val prf_asm = "proof-asm";
   val prf_script = "proof-script";
 
-  val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
-    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
+  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
+    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
 end;