diff -r 1800e7134d2e -r 8c8eafb63746 src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Fri Jul 12 16:41:39 2002 +0200 +++ b/src/HOL/Bali/Trans.thy Fri Jul 12 17:16:22 2002 +0200 @@ -10,47 +10,7 @@ *) theory Trans = Evaln: -(* -constdefs inj_stmt:: "stmt \ term" ("\_\\<^sub>s" 83) - "\s\\<^sub>s \ In1r s" -constdefs inj_expr:: "expr \ term" ("\_\\<^sub>e" 83) - "\e\\<^sub>e \ In1l e" -*) -axclass inj_term < "type" -consts inj_term:: "'a::inj_term \ term" ("\_\" 83) - -instance stmt::inj_term .. - -defs (overloaded) -stmt_inj_term_def: "\c::stmt\ \ In1r c" - -lemma stmt_inj_term_simp: "\c::stmt\ = In1r c" -by (simp add: stmt_inj_term_def) - -instance expr::inj_term .. - -defs (overloaded) -expr_inj_term_def: "\e::expr\ \ In1l e" - -lemma expr_inj_term_simp: "\e::expr\ = In1l e" -by (simp add: expr_inj_term_def) - -instance var::inj_term .. - -defs (overloaded) -var_inj_term_def: "\v::var\ \ In2 v" - -lemma var_inj_term_simp: "\v::var\ = In2 v" -by (simp add: var_inj_term_def) - -instance "list":: (type) inj_term .. - -defs (overloaded) -expr_list_inj_term_def: "\es::expr list\ \ In3 es" - -lemma expr_list_inj_term_simp: "\es::expr list\ = In3 es" -by (simp add: expr_list_inj_term_def) constdefs groundVar:: "var \ bool" "groundVar v \ (case v of