equal
deleted
inserted
replaced
383 (* main case *) |
383 (* main case *) |
384 by (clarify_tac set_cs 1); |
384 by (clarify_tac set_cs 1); |
385 by (pair_tac "ex" 1); |
385 by (pair_tac "ex" 1); |
386 by (Seq_case_simp_tac "y" 1); |
386 by (Seq_case_simp_tac "y" 1); |
387 (* UU case *) |
387 (* UU case *) |
388 by (asm_full_simp_tac (simpset() addsimps [UU_is_Conc])1); |
388 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1); |
389 (* nil case *) |
389 (* nil case *) |
390 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1); |
390 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1); |
391 (* cons case *) |
391 (* cons case *) |
392 by (pair_tac "aa" 1); |
392 by (pair_tac "aa" 1); |
393 by Auto_tac; |
393 by Auto_tac; |