equal
deleted
inserted
replaced
55 |
55 |
56 (* |
56 (* |
57 -------- (init) |
57 -------- (init) |
58 C \<Longrightarrow> #C |
58 C \<Longrightarrow> #C |
59 *) |
59 *) |
60 fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI; |
60 fun init C = Thm.instantiate (TVars.empty, Vars.make1 ((("A", 0), propT), C)) Drule.protectI; |
61 |
61 |
62 (* |
62 (* |
63 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C |
63 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C |
64 ------------------------ (protect n) |
64 ------------------------ (protect n) |
65 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> #C |
65 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> #C |