src/HOL/ex/meson.ML
changeset 1512 ce37c64244c0
parent 1465 5d7a7e439cec
child 1585 c44a012cf950
     1.1 --- a/src/HOL/ex/meson.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/HOL/ex/meson.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -158,12 +158,10 @@
     1.4  val prop_of = #prop o rep_thm;
     1.5  
     1.6  (*Permits forward proof from rules that discharge assumptions*)
     1.7 -fun forward_res nf state =
     1.8 -  case Sequence.pull
     1.9 -        (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), 
    1.10 -                state))
    1.11 +fun forward_res nf st =
    1.12 +  case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
    1.13    of Some(th,_) => th
    1.14 -   | None => raise THM("forward_res", 0, [state]);
    1.15 +   | None => raise THM("forward_res", 0, [st]);
    1.16  
    1.17  
    1.18  (*Negation Normal Form*)
    1.19 @@ -188,10 +186,10 @@
    1.20  fun skolemize th = 
    1.21    if not (has_consts ["Ex"] (prop_of th)) then th
    1.22    else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.23 -                          disj_exD, disj_exD1, disj_exD2]))
    1.24 +			      disj_exD, disj_exD1, disj_exD2]))
    1.25      handle THM _ => 
    1.26          skolemize (forward_res skolemize
    1.27 -                (tryres (th, [conj_forward, disj_forward, all_forward])))
    1.28 +		   (tryres (th, [conj_forward, disj_forward, all_forward])))
    1.29      handle THM _ => forward_res skolemize (th RS ex_forward);
    1.30  
    1.31  
    1.32 @@ -243,8 +241,7 @@
    1.33          (METAHYPS (resop (cnf_nil seen)) 1) THEN
    1.34          (STATE (fn st' => 
    1.35                  METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
    1.36 -    in  Sequence.list_of_s (tapply(tac, th RS disj_forward))  @  ths
    1.37 -    end
    1.38 +    in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
    1.39  and cnf_nil seen th = cnf_aux seen (th,[]);
    1.40  
    1.41  (*Top-level call to cnf -- it's safe to reset name_ref*)
    1.42 @@ -266,13 +263,13 @@
    1.43  qed "disj_forward2";
    1.44  
    1.45  (*Forward proof, passing extra assumptions as theorems to the tactic*)
    1.46 -fun forward_res2 nf hyps state =
    1.47 +fun forward_res2 nf hyps st =
    1.48    case Sequence.pull
    1.49 -        (tapply(REPEAT 
    1.50 -           (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), 
    1.51 -           state))
    1.52 +        (REPEAT 
    1.53 +	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
    1.54 +	 st)
    1.55    of Some(th,_) => th
    1.56 -   | None => raise THM("forward_res2", 0, [state]);
    1.57 +   | None => raise THM("forward_res2", 0, [st]);
    1.58  
    1.59  (*Remove duplicates in P|Q by assuming ~P in Q
    1.60    rls (initially []) accumulates assumptions of the form P==>False*)