little Bugfix
authorschirmer
Fri Jul 12 17:16:22 2002 +0200 (2002-07-12)
changeset 133548c8eafb63746
parent 13353 1800e7134d2e
child 13355 d19cdbd8b559
little Bugfix
src/HOL/Bali/Trans.thy
     1.1 --- a/src/HOL/Bali/Trans.thy	Fri Jul 12 16:41:39 2002 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Fri Jul 12 17:16:22 2002 +0200
     1.3 @@ -10,47 +10,7 @@
     1.4  *)
     1.5  
     1.6  theory Trans = Evaln:
     1.7 -(*
     1.8 -constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
     1.9 -    "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
    1.10  
    1.11 -constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
    1.12 -    "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
    1.13 -*)
    1.14 -axclass inj_term < "type"
    1.15 -consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
    1.16 -
    1.17 -instance stmt::inj_term ..
    1.18 -
    1.19 -defs (overloaded)
    1.20 -stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.21 -
    1.22 -lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    1.23 -by (simp add: stmt_inj_term_def)
    1.24 -
    1.25 -instance expr::inj_term ..
    1.26 -
    1.27 -defs (overloaded)
    1.28 -expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.29 -
    1.30 -lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    1.31 -by (simp add: expr_inj_term_def)
    1.32 -
    1.33 -instance var::inj_term ..
    1.34 -
    1.35 -defs (overloaded)
    1.36 -var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.37 -
    1.38 -lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
    1.39 -by (simp add: var_inj_term_def)
    1.40 -
    1.41 -instance "list":: (type) inj_term ..
    1.42 -
    1.43 -defs (overloaded)
    1.44 -expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
    1.45 -
    1.46 -lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
    1.47 -by (simp add: expr_list_inj_term_def)
    1.48  
    1.49  constdefs groundVar:: "var \<Rightarrow> bool"
    1.50  "groundVar v \<equiv> (case v of