# HG changeset patch
# User kleing
# Date 1363614440 -3600
# Node ID daac447f0e9361f35b23218d52193e0b3f74e035
# Parent  9ac7868ae64fd5d98e6389ca51f7af9e8fde2eca
managed to eliminate further snippets

diff -r 9ac7868ae64f -r daac447f0e93 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Mon Mar 18 14:27:38 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Mar 18 14:47:20 2013 +0100
@@ -5,7 +5,6 @@
 
 subsection "Syntax Directed Typing"
 
-text_raw{*\snip{sectypeDef}{0}{2}{% *}
 inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
 Skip:
   "l \<turnstile> SKIP" |
@@ -17,7 +16,6 @@
   "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
 While:
   "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
-text_raw{*}%endsnip*}
 
 code_pred (expected_modes: i => i => bool) sec_type .
 
@@ -183,7 +181,6 @@
 computation by an antimonotonicity rule. We introduce the standard system now
 and show the equivalence with our formulation. *}
 
-text_raw{*\snip{sectypepDef}{0}{2}{% *}
 inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
 Skip':
   "l \<turnstile>' SKIP" |
@@ -197,7 +194,6 @@
   "\<lbrakk> sec b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
 anti_mono':
   "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
-text_raw{*}%endsnip*}
 
 lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
 apply(induction rule: sec_type.induct)
@@ -219,7 +215,6 @@
 
 subsection "A Bottom-Up Typing System"
 
-text_raw{*\snip{sectypebDef}{0}{2}{% *}
 inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
 Skip2:
   "\<turnstile> SKIP : l" |
@@ -232,7 +227,6 @@
   \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
 While2:
   "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
-text_raw{*}%endsnip*}
 
 
 lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"