# HG changeset patch
# User kleing
# Date 1363613258 -3600
# Node ID 9ac7868ae64fd5d98e6389ca51f7af9e8fde2eca
# Parent  d2bc229e1f37cf60b6ac8dfe505fbebbd0ecc287
fewer IMP snippets

diff -r d2bc229e1f37 -r 9ac7868ae64f src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Mon Mar 18 13:18:42 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Mon Mar 18 14:27:38 2013 +0100
@@ -11,7 +11,6 @@
 
 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
 
-text_raw{*\snip{tavalDef}{0}{2}{% *}
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |
 "taval (Rc r) s (Rv r)" |
@@ -20,7 +19,6 @@
  \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
  \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
-text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "taval (Ic i) s v"  "taval (Rc i) s v"
@@ -31,14 +29,12 @@
 
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
-text_raw{*\snip{tbvalDef}{0}{2}{% *}
 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
 "tbval (Bc v) s v" |
 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
-text_raw{*}%endsnip*}
 
 subsection "Syntax of Commands"
 (* a copy of Com.thy - keep in sync! *)
@@ -53,7 +49,6 @@
 
 subsection "Small-Step Semantics of Commands"
 
-text_raw{*\snip{tsmallstepDef}{0}{2}{% *}
 inductive
   small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -66,7 +61,6 @@
 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
-text_raw{*}%endsnip*}
 
 lemmas small_step_induct = small_step.induct[split_format(complete)]
 
@@ -76,7 +70,6 @@
 
 type_synonym tyenv = "vname \<Rightarrow> ty"
 
-text_raw{*\snip{atypingDef}{0}{2}{% *}
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
 where
@@ -84,30 +77,25 @@
 Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
 V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
 Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
-text_raw{*}%endsnip*}
 
 text{* Warning: the ``:'' notation leads to syntactic ambiguities,
 i.e. multiple parse trees, because ``:'' also stands for set membership.
 In most situations Isabelle's type system will reject all but one parse tree,
 but will still inform you of the potential ambiguity. *}
 
-text_raw{*\snip{btypingDef}{0}{2}{% *}
 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
 where
 B_ty: "\<Gamma> \<turnstile> Bc v" |
 Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
 And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
-text_raw{*}%endsnip*}
 
-text_raw{*\snip{ctypingDef}{0}{2}{% *}
 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
 Skip_ty: "\<Gamma> \<turnstile> SKIP" |
 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
 Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
-text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;c2"