diff -r d199410f1db1 -r 968d2dccf2de set.ML --- a/set.ML Mon Oct 04 15:43:54 1993 +0100 +++ b/set.ML Thu Oct 07 10:20:30 1993 +0100 @@ -42,7 +42,7 @@ val bspec = result(); val major::prems = goalw Set.thy [Ball_def] - "[| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"; + "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"; by (rtac (major RS spec RS impCE) 1); by (REPEAT (eresolve_tac prems 1)); val ballE = result(); @@ -109,7 +109,7 @@ (*Classical elimination rule*) val major::prems = goalw Set.thy [subset_def] - "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"; + "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"; by (rtac (major RS ballE) 1); by (REPEAT (eresolve_tac prems 1)); val subsetCE = result(); @@ -153,7 +153,7 @@ val equalityE = result(); val major::prems = goal Set.thy - "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"; + "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; by (rtac (major RS equalityE) 1); by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); val equalityCE = result(); @@ -179,7 +179,7 @@ Negated assumptions behave like formulae on the right side of the notional turnstile...*) val major::prems = goalw Set.thy [Compl_def] - "[| c : Compl(A) |] ==> ~c:A"; + "[| c : Compl(A) |] ==> c~:A"; by (rtac (major RS CollectD) 1); val ComplD = result(); @@ -197,7 +197,7 @@ val UnI2 = result(); (*Classical introduction rule: no commitment to A vs B*) -val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B" +val UnCI = prove_goal Set.thy "(c~:B ==> c:A) ==> c : A Un B" (fn prems=> [ (rtac classical 1), (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), @@ -236,7 +236,7 @@ (*** Set difference ***) val DiffI = prove_goalw Set.thy [set_diff_def] - "[| c : A; ~ c : B |] ==> c : A - B" + "[| c : A; c ~: B |] ==> c : A - B" (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]); val DiffD1 = prove_goalw Set.thy [set_diff_def] @@ -249,12 +249,12 @@ [rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]); val DiffE = prove_goal Set.thy - "[| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P" + "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" (fn prems=> [ (resolve_tac prems 1), (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); -val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & ~ c:B)" +val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & c~:B)" (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]); @@ -294,7 +294,7 @@ (fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]); (*Classical introduction rule*) -val insertCI = prove_goal Set.thy "(~a:B ==> a=b) ==> a: insert(b,B)" +val insertCI = prove_goal Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)" (fn [prem]=> [ (rtac (disjCI RS (insert_iff RS iffD2)) 1), (etac prem 1) ]); @@ -358,7 +358,7 @@ (*"Classical" elimination -- by the Excluded Middle on a:A *) val major::prems = goalw Set.thy [INTER_def] - "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R"; + "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R"; by (rtac (major RS CollectD RS ballE) 1); by (REPEAT (eresolve_tac prems 1)); val INT_E = result(); @@ -430,7 +430,7 @@ (*"Classical" elimination rule -- does not require proving X:C *) val major::prems = goalw Set.thy [Inter_def] - "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R"; + "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R"; by (rtac (major RS INT_E) 1); by (REPEAT (eresolve_tac prems 1)); val InterE = result();