src/HOL/Option.ML
changeset 4477 b3e5857d8d99
parent 4133 0a08c2b9b1ed
child 4752 1c334bd00038
     1.1 --- a/src/HOL/Option.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Option.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  open Option;
     1.5  
     1.6  qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
     1.7 -	(K [option.induct_tac "x" 1, Auto_tac()]);
     1.8 +	(K [option.induct_tac "x" 1, Auto_tac]);
     1.9  
    1.10  section "case analysis in premises";
    1.11  
    1.12 @@ -31,7 +31,7 @@
    1.13  	res_inst_tac [("opt","x")] optionE 1,
    1.14  	 forward_tac prems 1,
    1.15  	  forward_tac prems 3, 
    1.16 -	   Auto_tac()]);
    1.17 +	   Auto_tac]);
    1.18  fun option_case_tac i = EVERY [
    1.19  	etac option_caseE i,
    1.20  	 hyp_subst_tac (i+1),
    1.21 @@ -56,4 +56,4 @@
    1.22  val option_map_SomeD = prove_goalw thy [option_map_def]
    1.23  	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
    1.24  	optionE_tac "x" 1,
    1.25 -	 Auto_tac()]);
    1.26 +	 Auto_tac]);