src/HOL/Option.ML
changeset 2056 93c093620c28
parent 2031 03a843f0f447
child 2935 998cb95fdd43
     1.1 --- a/src/HOL/Option.ML	Mon Oct 07 10:26:00 1996 +0200
     1.2 +++ b/src/HOL/Option.ML	Mon Oct 07 10:28:44 1996 +0200
     1.3 @@ -27,5 +27,4 @@
     1.4  by (option.induct_tac "opt" 1);
     1.5  by (Simp_tac 1);
     1.6  by (Asm_full_simp_tac 1);
     1.7 -by (Fast_tac 1);
     1.8  qed"expand_option_case";