equal
deleted
inserted
replaced
70 handle CTERM _ => Seq.empty |
70 handle CTERM _ => Seq.empty |
71 *} |
71 *} |
72 |
72 |
73 |
73 |
74 lemma trueprop_cong: |
74 lemma trueprop_cong: |
75 shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)" |
75 shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)" |
76 by auto |
76 by auto |
77 |
77 |
78 lemma list_induct_hol4: |
78 lemma list_induct_hol4: |
79 fixes P :: "'a list ⇒ bool" |
79 fixes P :: "'a list \<Rightarrow> bool" |
80 assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))" |
80 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
81 shows "∀l. (P l)" |
81 shows "\<forall>l. (P l)" |
82 using a |
82 using a |
83 apply (rule_tac allI) |
83 apply (rule_tac allI) |
84 apply (induct_tac "l") |
84 apply (induct_tac "l") |
85 apply (simp) |
85 apply (simp) |
86 apply (metis) |
86 apply (metis) |
91 let |
91 let |
92 val ctxt = Variable.set_body false (Context.proof_of context); |
92 val ctxt = Variable.set_body false (Context.proof_of context); |
93 val ((_, [th']), _) = Variable.import true [th] ctxt; |
93 val ((_, [th']), _) = Variable.import true [th] ctxt; |
94 in th' end); |
94 in th' end); |
95 *} |
95 *} |
|
96 |
|
97 (*lemma equality_twice: |
|
98 "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)" |
|
99 by auto*) |