1.1 --- a/src/HOL/simpdata.ML Tue Oct 10 09:17:17 2006 +0200
1.2 +++ b/src/HOL/simpdata.ML Tue Oct 10 09:17:18 2006 +0200
1.3 @@ -276,9 +276,9 @@
1.4 else error "Conclusion of congruence rules must be =-equality"
1.5 end);
1.6
1.7 -(* Elimination of True from asumptions: *)
1.8 +(* Elimination of True from assumptions: *)
1.9
1.10 -local fun rd s = read_cterm (sign_of (the_context())) (s, propT);
1.11 +local fun rd s = read_cterm (the_context()) (s, propT);
1.12 in val True_implies_equals = standard' (equal_intr
1.13 (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI))
1.14 (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P")))));